Hybrid verifications of reactive programs

Olivier Roux*, Vlad Rusu, Franck Cassez

*Corresponding author for this work

Research output: Contribution to journalArticle

1 Citation (Scopus)

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.

Original languageEnglish
Pages (from-to)448-471
Number of pages24
JournalFormal Aspects of Computing
Volume11
Issue number4
Publication statusPublished - 1999

Keywords

  • Asynchronism
  • Hybrid system
  • Model checking
  • Reactive system
  • Real time

Fingerprint Dive into the research topics of 'Hybrid verifications of reactive programs'. Together they form a unique fingerprint.

  • Cite this