Verification of an active control system using temporal process algebra |
| |
Authors: | Wael M. Elseaidy John W. Baugh Jr Rance Cleaveland |
| |
Affiliation: | (1) Department of Civil Engineering, North Carolina State University, 27695 Raleigh, NC, USA;(2) Department of Computer Science, North Carolina State University, Raleigh, USA |
| |
Abstract: | In this paper we describe complementary approaches that can be used to ensure the reliability of real-time systems, such as those used in active structural control systems. These approaches include both model-checking and simulation, and are based on a temporal process algebra. We combine these formal methods with a high-level, graphical modeling technique, Modechart, to specify an active structural control system consisting of several processors. Timing requirements on the system are specified and verified with a combination of process algebraic models and modal logic, and various simulation concepts are described for debugging models and for gaining insight into system behavior. |
| |
Keywords: | Active structural control Calculus of communicating systems (CCS) Concurrency workbench Modechart Real-time systems Simulation Temporal CCS |
本文献已被 SpringerLink 等数据库收录! |
|