Title :
Verifying an intelligent structural control system: a case study
Author :
Elseaidy, Wael M. ; Cleaveland, Rance ; Baugh, John W., Jr.
Author_Institution :
Dept. of Civil Eng., North Carolina State Univ., Raleigh, NC, USA
Abstract :
Describes the formal verification of the timing properties of the design of an intelligent structural control system using the Concurrency Workbench, an automatic verification tool for finite-state processes. The high-level design of the system is first given in Modechart, a graphical specification language for real-time systems, and then translated into a temporal process algebra supported by the Workbench. The facilities provided by this tool are then used to analyze the system and ultimately show it to be correct
Keywords :
distributed control; distributed processing; finite automata; formal verification; intelligent control; process algebra; real-time systems; specification languages; structural engineering computing; temporal logic; time-varying systems; timing; visual languages; Concurrency Workbench; Modechart; automatic verification tool; case study; finite-state processes; formal verification; graphical specification language; high-level design; intelligent structural control system verification; temporal process algebra; timing properties; Distributed computing; Distributed control; Finite automata; Intelligent control; Logic; Real time systems; Specification languages; Time-varying systems; Timing; Visual languages;
Conference_Titel :
Real-Time Systems Symposium, 1994., Proceedings.
Conference_Location :
San Juan
Print_ISBN :
0-8186-6600-5
DOI :
10.1109/REAL.1994.342708