Verifying an intelligent structural control system: a case study

TitleVerifying an intelligent structural control system: a case study
Publication TypeConference Papers
Year of Publication1994
AuthorsElseaidy WM, Cleaveland R, Baugh JW
Conference NameReal-Time Systems Symposium, 1994., Proceedings.
Date Published1994/12/07/9
ISBN Number0-8186-6600-5
Keywordsautomatic verification tool, case study, Concurrency Workbench, Distributed computing, Distributed control, distributed processing, finite automata, finite-state processes, formal verification, graphical specification language, high-level design, intelligent control, intelligent structural control system verification, Logic, Modechart, Process algebra, Real time systems, real-time systems, Specification languages, structural engineering computing, temporal logic, temporal process algebra, time-varying systems, Timing, timing properties, visual languages

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