Automatic real-time analysis of reactive systems with the PARTS toolset Real-time systems are becoming increasingly widespread, often in safety-critical applications. It is therefore crucial that these systems be correct; however, there are few automated tools for analyzing concurrency and timing properties of these systems. The PARTS toolset uses a Petri-net-based reachability analysis to analyze program specifications written in an Ada-83 subset. Our simple time Petri nets are specifically aimed at facilitating real-time analysis. In order to control the state-explosion problem, PARTS employs several optimization techniques aimed at state-space reduction. In this paper we discuss our approach and we report on extensive experiments with several examples of real-time specifications based on Ada 83. When possible, we also compare our experimental results with results obtained by other approaches to real-time analysis.
Keywords for this software
References in zbMATH (referenced in 2 articles )
Showing results 1 to 2 of 2.
- Iordache, Marian V.; Antsaklis, Panos J.: Supervisory control of concurrent systems. A Petri net structural approach. (2006)
- Buy, U.; Sloan, R. H.: Automatic real-time analysis of reactive systems with the PARTS toolset (2001)