Integrated architectural modeling and analysis for high-assurance command and control system design

A real-time architectural specification (RAS) approach and its application to command and control (C2) systems are presented. The objective is to establish a formal foundation that will enable us to integrate existing rich but fragmented formal techniques for system specification and verification into practical and scaleable formal engineering methods to support the design and development of highly reliable real-time distributed systems. The contribution of RAS is twofold; first, it provides a formal system that integrates the system´s timing requirements and the propagation of the requirements into the process of architectural modeling and design and provides a systematic way to enforce that the requirements are met in every step of the design process. Second, it offers an incremental and more scalable approach for design modeling. These two features together make RAS a suitable model for the design of C2 systems. Based on these features, we further present an incremental method for verifying timing properties of a RAS model that helps to reduce the complexity of analysis both at a given design level or across different design levels