Incremental architectural modeling and verification of real-time concurrent systems

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