Papyrus-RT is an open-source modelling tool based on the concept of Model-Driven Engineering and is capable of generating executable C++ codes. It is intended for designing and developing complex, real-time, embedded systems. The modeling component of Papyrus-RT offers UML-RT for specifying software systems.

 nuXmv on the other hand is a model checker, that can verify system models against a set of properties defined using temporal logics.

 As a part of the project work, each team comprising of 2-4 students, would need to perform the following set of activities -

  1. model a given example in the Papyrus-RT tool.
  2. compile and run their model and verify the model semantics using test cases.
  3. use a given set of rules to mechanically translate their model into an equivalent nuXmv model.
  4. verify this model against a set of system properties relevant for their example

 

Systems like the Airport Conveyer Belt, Car Door Lock, Car Air Bag, Human Pacemaker, Parcel routing, Traffic Light or River Basin Management, could be chosen as an example for the project.