A Component-Based Approach to Verification of Embedded Control Systems Using TLA+

Software running in embedded systems necessary acquires some properties of the physical world. Usually, these properties form a part of non-functional aspects in system requirements. To model embedded software, these aspects must be considered by a specification method otherwise the model of a system easily diverges from the reality and becomes inapplicable in further refinement and analysis. Constructing large systems relies on effective and systematic application of modular approach. A large class of entities playing the role of building blocks that can be composed have been defined, most notably, classes for object-oriented program construction, components in hardware design, procedures and modules in procedural programming, and active objects and actors for reactive programming.