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.

Networked cybernetic and physical systems of the Internet of Things (IoT) immerse civilian and industrial infrastructures into an interconnected and dynamic web of hybrid and mobile devices. The key feature of such systems is the hybrid and tight coupling of mobile and pervasive discrete communications in a continuously evolving environment (discrete computations with predominant continuous dynamics). In the aim of ensuring the correctness and reliability of such heterogeneous infrastructures, we introduce the hybrid π -calculus ( H p C ), to formally capture both mobility, pervasiveness and hybridisation in infrastructures where the network topology and its communicating entities evolve continuously in the physical world. The π -calculus proposed by Robin Milner et al. is a process calculus that can model mobile communications and computations in a very elegant manner. The H p C we propose is a conservative extension of the classical π -calculus, i.e., the extension is “minimal”, and yet describes mobility, time and physics of systems, while allowing to lift all theoretical results (e.g. bisimulation) to the context of that extension. We showcase the H p C by considering a realistic handover protocol among mobile devices.

Model-based design has become the predominant approach to the design of hybrid and cyber-physical systems (CPSs). It advocates the use of mathematically founded models to capture heterogeneous digital and analog behaviours from domain-specific formalisms, allowing all engineering tasks of verification, code synthesis, and validation to be performed within a single semantic body. Guaranteeing the consistency among the different views and heterogeneous models of a system at different levels of abstraction, however, poses significant challenges. To address these issues, Hoare and He’s Unifying Theories of Programming (UTP) proposes a calculus to capture domain-specific programming and modelling paradigms into a unified semantic framework. Our goal is to extend UTP to form a semantic foundation for CPS design. Higher-order UTP (HUTP) is a conservative extension to Hoare and He’s theory that supports the specification of discrete, real-time, and continuous dynamics, concurrency and communication, and higher-order quantification. Within HUTP, we define a calculus of normal hybrid designs to model, analyse, compose, refine, and verify heterogeneous hybrid system models. In addition, we define respective formal semantics for Hybrid Communicating Sequential Processes and Simulink using HUTP.

We give an introduction to the MARS toolchain for formal modeling and verification of hybrid systems. It consists of translators from Simulink/Stateflow models to Hybrid Communicating Sequential Processes (HCSP), and tools for simulation, code generation, and deductive verification of an HCSP model. We apply the toolchain to model the descent guidance control phase of the recently launched Tianwen I mars lander, and verify that it correctly controls the velocity of the lander.