Automatic Real-Time Analysis of Reactive Systems with the PARTS Toolset |
| |
Authors: | U. Buy R.H. Sloan |
| |
Affiliation: | (1) Electrical Engineering and Computer Science (M/C 154), University of Illinois, 851 South Morgan Street, Chicago, Illinois 60607, USA |
| |
Abstract: | 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: | real-time verification real-time systems automated analysis experimental evaluation Petri nets |
本文献已被 SpringerLink 等数据库收录! |
|