Title :
An integrated approach to modeling and analysis of embedded real-time systems based on Timed Petri Nets
Author :
Gu, Zonghua ; Shin, Kang G.
Author_Institution :
Dept. of Electr. Eng. & Comput. Sci., Michigan Univ., Ann Arbor, MI, USA
Abstract :
In computer-based control systems, embedded software is taking over what mechanical and dedicated electronic systems used to do, that is, to engage and control the physical world, interacting directly with sensors and actuators. Therefore, software running on a digital processor is tightly-coupled with its surrounding physical environment. We propose an integrated approach based on Timed Petri-Nets for modeling and analysis of embedded real-time systems where real-time scheduling behavior of the controller software is explicitly represented at the model-level, together with the physical environment that it interacts with. This enables the designer to have an integrated view of the entire system while analyzing the system and making design decisions. We also describe a syntax-directed, automated translation procedure from Timed Petri-Nets to Timed Automata, thus enabling the use of model checkers such as UPPAAL for analysis purposes. We consider the railroad crossing problem as an application example, and evaluate alternatives for controller implementation on either single-processor or distributed multi-processor platforms based on the integrated approach.
Keywords :
Petri nets; embedded systems; formal verification; multiprocessing systems; parallel machines; processor scheduling; Petri nets; UPPAAL model checker; automated translation procedure; controller software; digital processor; distributed multiprocessor scheduling; embedded real-time system; embedded software; timed automata; Actuators; Automatic control; Control systems; Embedded computing; Embedded software; Mechanical sensors; Petri nets; Physics computing; Real time systems; Sensor systems;
Conference_Titel :
Distributed Computing Systems, 2003. Proceedings. 23rd International Conference on
Print_ISBN :
0-7695-1920-2
DOI :
10.1109/ICDCS.2003.1203484