Design Validation of Multi-Mode Systems

Cyber-Physical Systems (CPS) are involved with both physical processes and com- putational processes. The interaction of physical components and computational components makes it difficult to analyze, design and verify this type of systems. The problem becomes more complex when an input or decision must be initiated by a human. For this dissertation, Cyber-Physical Systems with a human operator in the loop are called Embedded Human Systems (EHS). To ensure the safety of EHS such as traffic control systems, space shuttle control systems, nuclear power plant control systems and so on, it is critically important for human operators to fully understand both physical and computational processes. However, humans are usually easily overwhelmed by concurrent information, so this assumption becomes intractable when it comes to complex EHS with timing constraints.

This dissertation proposes a domain specific modeling language that takes ad- vantage of hybrid system abstraction to retain important system behaviors and automatically generates self-configured system verification software. The verifica- tion software effectively reduces the computation time through parallel scheduling algorithm, and if the computation process detects a violation of the design require- ments, verification can be halted without wasting computation resources. The mod- eling environment also allows a user to conveniently set design constraints to avoid flaws early in the prototype process, and reuse the available model for a family of different platforms. Several verification results of different platforms are shown to demonstrate the efficiency and reusability of the modeling environment.