Title :
Incremental architectural modeling and verification of real-time concurrent systems
Author :
Deng, Yi ; Wang, Jiacun ; Sinha, Rakesh
Author_Institution :
Sch. of Comput. Sci., Florida Int. Univ., Miami, FL, USA
Abstract :
An incremental approach for architectural modeling and analysis of real-time concurrent systems is presented. The approach integrates existing formal methods, more specifically time Petri nets and real-time computational tree logic, and leverages their complementary strengths in a way that allows us to systematically enforce that architectural design meets the system´s timing requirements, and to incrementally verify the conformance. Consequently, our approach is able to provide better assurance to system design and yet reduce the complexity of analysis. The approach is based on a Real-time Architectural Specification (RAS) model, which provides a formal basis to systematically maintain a correlation between the (timing) requirements of a system and its architectural design. Based on RAS, we further present a method to verify timing properties of a system design. This method helps conquer the complexity of analysis in two dimensions. Horizontally at each design level, incremental verification is achieved by introducing TPN reduction rules that allow us to compose analysis results on individual system components. Vertically across design levels, incremental verification is achieved by propagating higher-level constraints to lower-level designs so that we can safely plug a component design into a high-level architecture without having to re-verify the entire model. A naval command and control (C2) system is used throughout the paper to demonstrate the concept and usability of our approach
Keywords :
Petri nets; command and control systems; concurrency theory; formal logic; formal specification; parallel programming; program verification; real-time systems; software architecture; RAS model; Real-time Architectural Specification; architectural modeling; component design; formal methods; incremental approach; naval command and control system; real-time computational tree logic; real-time concurrent systems; system design; system verification; time Petri nets; timing requirements; usability; Air traffic control; Computer science; Control systems; Logic design; Manufacturing systems; Petri nets; Plugs; Real time systems; System analysis and design; Timing;
Conference_Titel :
Formal Engineering Methods, 1998. Proceedings. Second International Conference on
Conference_Location :
Brisbane, Qld.
Print_ISBN :
0-8186-9198-0
DOI :
10.1109/ICFEM.1998.730567