Scenario-Based Specification of Automotive Requirements With Quantitative Constraints and Synthesis of SL/SF Monitors

摘要

Requirements of embedded systems often describe the system behavior with quantitative constraints over parameters such as timing, memory, and other resources. In this letter, we present a visual language suited for scenario-based specification of requirements with quantitative constraints. Our language, known as event sequence charts with quantitative constraints (ESC-QC), is inspired by message sequence charts (MSC) and its variants. We introduce ESC-QC notations through an example from automotive requirements and then describe the formal syntax and semantics. Besides being useful for formal documentation and analysis of system requirements, ESC-QC specifications can be translated into monitors and used for run-time verification of designs. In automotive systems Simulink/Stateflow (SL/SF) is widely used for design of control systems. We have developed an algorithm for automatic synthesis of SL/SF monitors from ESC-QC specifications. We have used this algorithm for generating monitors for verification of controller models from active safety and body control applications.