Modeling and Verification of Hybrid Systems by Extending AADL

System-level design, and dependability prediction of safety-critical systems demand integration of architectural and analysis artifacts in a single development environment. Hybrid systems, with mutual dependencies and extensive interactions between the control portion and its physical environment, further intensify this need. Architecture Analysis and Design Language (AADL) is a model-based engineering language for the architectural design and analysis of embedded control systems. Core AADL has been extended with sub-languages for modeling and analysis of discrete behavior of the control portion, but not for continuous behavior of the physical environment. In a previous work, we have introduced Hybrid Annex for continuous behavior modeling as part of initial findings of an ongoing research effort on fulfilling the need for integrated modeling of the computing system along with its physical environment. In this article, we first detail complete structure of the Hybrid Annex along with appropriate examples for each section. Then, we present formal semantics of the synchronous subset of AADL models annotated with Hybrid Annex specifications using Hybrid Communicating Sequential Processes (HCSP). Formal semantics are used to verify correctness of AADL models (with Hybrid Annex specifications) using Hybrid Hoare Logic (HHL). A case study on a realistically-scaled automatic cruise control system is provided to demonstrate modeling and verification of hybrid systems using AADL with the proposed extension.