Runtime enforcement of reactive systems (compositionality of enforcers)

Potential supervisors: 
Description: 

 

Runtime monitoring and enforcement

Runtime verification (RV) techniques deal with dynamically verifying a set of desirable properties over an execution of a “black-box” system. An alternative to such passive runtime analysis is runtime enforcement (RE).  Runtime enforcement techniques deal with synthesising an enforcer to observe the executions of a black-box system to ensure that a set of desired properties are satisfied. In the event of a violation, the enforcer performs certain evasive actions (delaying/suppressing/.. actions) so as to prevent the violation.

Runtime enforcement of reactive systems

A synchronous reactive system is non-terminating and interacts continuously with the adjoining environment. Examples of such systems include cardiac pacemakers (which must react to stimulus provided by the heart), and controllers in automotive systems. Closed-loop (bi-directional) runtime enforcement of reactive systems has been studied, where an enforcer can be synthesized for a given property [1, 2].

The project

For any complex safety-critical system, we generally have several safety properties to enforce. This project involves studying compositionality of enforcers i.e., how to compose two or more enforcers such that the composed enforcer satisfies some desired conditions. Compositionality of enforcers has been studied in a different setting e.g., see [3]. This project involves studying compositionality for reactive systems proposed in [1,2]. Compositionality of enforcers for reactive systems will be different from [3] and more challenging since the enforcement mechanism in [1,2] allows editing and is bi-directional.

One of the constraints for reactive systems is that it the enforcer cannot halt/block. Thus, compositionality may also involve checking whether a given set of properties are conflicting, and approaches to resolve them.

The work will also involve extending existing implementations proposed for mechanisms in [1,2] to handle compositionality of enforcers, possibility for the student to explore on application/case study of their interest.

Related courses: Finite automata theory and formal languages, Formal Methods in Software Development

Prerequisites: Programming (Python, Java, C..), propositional logic, automata theory, interest/willingness to learn/explore/extend modelling, verification and synthesis tools.

Desired: Temporal logics and formal verification, formal modelling and verification tools

Contact: Srinivas Pinisetty (sripin@chalmers.se) and Gerardo Schneider (gersch@chalmers.se)

References

  1. Srinivas Pinisetty, Partha S. Roop, Steven Smyth, Stavros Tripakis, Reinhard von Hanxleden: Runtime enforcement of reactive systems using synchronous enforcers. SPIN 2017: 80-89
  2. S. Pinisetty, P. Roop, S. Smyth, N. Allen, S. Tripakis, and R. Hanxleden. Runtime Enforcement of Cyber-Physical Systems. ACM Trans. Embed. Comput. Syst. 16, 5s, Article 178 (September 2017), 25 pages. DOI: https://doi.org/10.1145/3126500 (Special Issue ESWEEK 2017)
  3. S. Pinisetty, S.Tripakis. Compositional Runtime Enforcement. In NASA Formal Methods Symposium (NFM), Minneapolis, USA, June 2016
Date range: 
October, 2017 to October, 2022