Self-Adaptive Actors (SEADA)
In SEADA we will use Ptolemy to represent the architecture, and extensions of Rebeca for modeling and verification. Ptolemy is a modeling and simulation tool for cyber-physical systems where the components are actors and the communication and coordination of actors are captured in a director which represents the Model of Computation. Rebeca is an actor-based modeling language with formal verification support. In SEADA, we will propose a framework for self-adaptive systems with a component-based architecture built in Ptolemy II. Our models@runtime will be coded in an extension of Probabilistic Timed Rebeca (with dynamic features), and supporting tools for customized run-time formal verification of these models will be developed. SEADA architecture in Ptolemy II forms the feedback loop and consists of four components of Monitor, Analyze, Plan, and Execute, together with a Knowledge-base, similar to the MAPE-K architecture. A Model of Computation for self-adaptive systems will be designed in Ptolemy. The distinctive feature of SEADA is its actor-based flavor which will reflect in the design of the components of the architecture, the models in the knowledge-base, and in the V&V and formal verification techniques. Ptolemy gives us the much-needed support to model and evaluate the system in a more abstract level, and the means to connect to the physical world, while Rebeca gives us the formal verification support for the model@runtime to assure safety concerns. Ptolemy components in SEADA call the external tools to verify models@runtime and check the safety in order to react accordingly. Before sending any command to the system for reconfiguration or change, they will check the safety of new configurations. Models in Dynamic Probabilistic Timed Rebeca, an actor-based language supporting dynamic and probabilistic behavior with timing constraints, will be the core models for runtime safety analysis. Probabilistic and statistical model checking and compositional verification will be the main analysis techniques in SEADA. We will create models on which we can zoom-in and zoom-out and reach to the necessary level of abstraction for the required analysis; we call these models magnifiable models. Instead of a predefined hierarchical or nested model, we will propose a flat model which can be modularized (partitioned) and be refined or abstracted (zoomed-in or zoomed-out) during runtime. The actor model serves as the model@runtime in the core of the knowledge-base of SEADA, and any dangerous situation will be reported to the Plan component to be dealt with. Our experience in specific state-space reduction techniques for actors, and bounded model checking empowered by heuristics, will be the foundation to build more agile runtime verification methods which are necessary for reliable and quick adaptation. In the following, we presented our model@runtime for two different application domains.
- The demo of our model@runtime for air traffic control: movie.
- The demo of our model@runtime for railway systems: movie.
Probabilistic Timed Rebeca
We developed a tool-set to generate Timed MDP semantics of PTRebeca model. The PTRebeca model is compiled by rmc-2.3.0 tool which is an executable jar file. Running rmc-2.3.0 tool generates corresponding C++ files. The resulted C++ files are compiled and executed to generate the state space of PTRebeca model in TMDP semantics. The generated state space is in the form of an XML file. We developed a Java program to get the XML file and generate the input file of PRISM. The input file of PRISM has an MDP module including the whole state space. Based on PTRebeca semantics, time progress is modeled by an integer-valued variable. By assigning rewards to transitions, we are able to check expected-time reachability and time-bounded probabilistic reachability properties.
The compiler does not support probabilistic assignment at this moment. To resolve this, before running rmc-2.3.0 tool, PTRebeca model should be simplified through replacing probabilistic assignments by non-deterministic assignments. Then, the simplified PTRebeca model is compiled by rmc-2.3.0 tool and C++ files are generated. C++ files are modified manually in the right places to retrieve the probabilistic assignments. Then, the resulted C++ files are compiled and executed to generate the state space of PTRebeca model in TMDP semantics.
Probabilistic Timed Rebeca examples are available here.
Timed Rebeca (TARO)
Building reliable software systems is a complex but important challenge of modern engineering. A fundamental determiner of software reliability is the methodology used to develop and verify both designs and implementations. Current tools have significant limitations that increase the cost and development time of software systems. There is no question that one of the fundamental tasks in computer and information science is advancing the state of our development methods: We need better techniques and tools for developing correct and predictable software systems.
Current methodologies are proved to be insufficient and ineffective in developing reliable and trustworthy distributed and asynchronous systems, specially when we are concerned about timing constraints. So, a main challenge of software engineering in future is to establish novel ideas, methods, and techniques for developing systems of this category. In the ICT (Information and Communication Technologies) work programme of 2010 of the European Commission, the first challenge is pervasive and trustworthy network and service infrastructures. At the same time formal analysis and verification are inevitable techniques to ensure dependability of systems.
In this project, we aim at contributing to this research effort. We propose to develop a methodology, techniques and tools, for building fully asynchronous systems, whose behaviour depends crucially on timing constraints, with associated formal analysis and verification support. Our methodology is based on proposing an actor-based modeling language, extended with timing constraints and supported by formal verification tools. The research emphasis in the project places it firmly at the core of the grand challenge of developing reliable networked systems, and at the leading edge of research in software engineering. The real-world case studies will be used as testbeds for establishing the applicability of the proposed methodology and of the associated tools. They will tie together the theoretical and practical aspects of the research, resulting in a substantial synergy.
Timed Rebeca examples are available here.
The goal of Sysfier is to develop an integrated environment for modeling and verifying SystemC designs by formalizing SystemC semantics and providing model checking tools. The tool Afra is developed to integrate Sytra, Modere and SyMon in addition to Rebeca and SystemC modeling environments. Afra gets SystemC models and LTL or CTL properties from the designer, and verifies the models. If a property is not satisfied, a counter- example is displayed. For verifying SystemC models, Afra translates SystemC codes to Rebeca using Sytra. It then utilizes the Rebeca verification tool set to verify the given properties. Where applicable, reduction techniques are used to tackle the state explosion problem.