PERTS: an environment for specification and verification of reactive systems

Bhattacharjee, A. K. ; Dhodapkara, S. D. ; Shyamasundar, R. K. (2001) PERTS: an environment for specification and verification of reactive systems Reliability Engineering & System Safety, 71 (3). pp. 299-310. ISSN 0951-8320

Full text not available from this repository.

Official URL:

Related URL:


In this paper, we describe the design and implementation of an environment for specification, analysis and verification of reactive systems. The environment allows the user to develop specification in the graphical formalism of Statecharts and analyze them using a simulation tool. A built-in translator tool translates the specification into an Esterel program for the purpose of carrying out verification. Through such an approach, we have been able to integrate the powerful graphical formalism of Statecharts, which is very appealing to engineers, and the power of the formal verification environment of Esterel. Since we translate Statecharts, which can be non-deterministic, to Esterel programs, which are fully deterministic, the system overcomes the non-determinism in the specifications by enforcing priority. The behavior of Esterel programs generated by the translator follow Harel and Naamad's 'step' semantics. In the paper, we describe the main components of the PERTS environment and the principles underlying the translation and illustrate the use of the system for specification and verification using an example.

Item Type:Article
Source:Copyright of this article belongs to Elsevier Science.
Keywords:Formal Specification and Verification; Reactive Systems; Synchronous Languages; Statecharts; Esterel; Translation; Programming Environment; Automata Reduction
ID Code:56600
Deposited On:24 Aug 2011 11:01
Last Modified:24 Aug 2011 11:01

Repository Staff Only: item control page