Compositional and Incremental Modeling and Analysis for High-Confidence Distributed Embedded Control Systems

Abstract

High confidence embedded control system software often requires formal analyses to ensure design correctness. Detailed models cover numerous design concerns such as controller stability, timing requirements, fault tolerance, and deadlock freedom. Models for each of these design domains must together provide a consistent and faithful representation of the potential problems an operational system would face. Coupling between separately designed components and modules prevents model analyses from scaling well to large designs. Coupling also occurs within individual systems and components between behaviors represented by different design concerns as different aspects of the design constrain design structures and parameters in conflicting ways. These complications combine with other factors to increase the difficulty of system integration, leading to high costs and long development schedules.

Correctness properties in model-based designs take one of the following forms (from Edwards et al): 1) Properties inherent to the model of computation, which hold for all valid specifications, 2) Syntactic properties which can be determined by analysis of the structure of specification elements, and 3) Semantic properties which require examination of the actual behavior of the specification.

To tackle problems associated with highly coupled designs, their required correctness constraints, and the cost impact on design projects, we have created the Embedded Systems Modeling Language (ESMoL). Well-formed models in ESMoL inherently express functional determinism (from dataflow semantics), deadlock-freedom (from synchrony), and timing determinism (from a time-triggered platform). To address more complex syntactic and semantic properties we propose incremental analysis, which allows us to extend previously calculated design analysis results to new features in an efficient way. We give an example of incremental syntactic analysis in the form of cycle checking to ensure well-formedness of ESMoL models. We give an example of incremental semantic analysis in scheduling dataflow graphs subject to end-to-end latency constraints. Effective incremental analysis techniques can allow developers to more rapidly iterate and converge on a correct design.