Hybrid verifications of reactive programs

Abstract

We present in this paper some new language features and constructs, that allow the joint synchronous/asynchronous programming of reactive applications, as well as their formal verification. We show that reactive applications may be dealt with from two points of view. First, from the chronological point of view, i.e., when reactions are instantaneous, generated by event occurrences in discrete time. Second, from the chronometrical point of view, when reactions have durations in dense time. This duality must be expressible in languages that allow a consistent programming of both synchronous and asynchronous features. The objective of mixing these dual approaches leads to model reactive systems by using hybrid systems, to deal simultaneously with both discrete and continuous phenomena. Furthermore, this must be followed by some verification of the application's properties, with respect to its behavioural and quantitative features. We analyze several existing frameworks that meet these requirements, and propose our own approach based on the language ELECTRE.