Cyber-Physical Systems (CPS) are smart systems integrating the physical and the computational world of increasing importance in a variety of domains, like healthcare, transportation, smart manufacturing. As their malfunctions can lead to critical incidents, their proper design and implementation are essential. My research objective was the elaboration of a method assuring the integrity, safety and reliability requirements of the system at design and run-time.
Building and managing CPSs is a very complex task. Dependability of a service delivered by a critical CPS necessitates the fulfillment of a variety of functional and extra-functional requirements.
System engineering has a variety of well-established design methodologies corresponding to the best industrial practice like NASA System Engineering Handbook or the NIST CPS Framework. Similarly, different reference architectures and platforms described by de-facto and industrial standards support component and (sub)system integration-based service implementation.
Formal proof of correctness of critical systems is a growing practical importance part. A complex CPS can include a multitude of components within and across architectural levels. The interaction between components is the primary source of faults in integration-based systems composition. Integration testing is mandatory, even if the components are typically pretested. Dependability assurance in dynamic CPS necessitates the extension of checking the interoperability from design-time to run-time.
My objective was to support the component integration by reusing component tests for integration testing and run-time verification. Our method extends the Assume-Guarantee approach for testing elaborated initially by NASA in the 90’s to a general-purpose run-time verification paradigm.
The new method supports the checking of the correctness of system integration starting of the formal description of the components (temporal logic expressions, state machines), the assumption on the operating environment by reusing the specific component tests.
Integration testing is carried out by waiving the test sequences of the individual components and simultaneously performing a formal check of the fulfillment of the assumption on operating conditions (pre-invariants) and the test oracles (post-invariants). A uniform model-based approach based on statecharts executes all the sequence, operating condition and output checking of the different components and facilitates the automated code generation of run-time checkers.
The OMG standard Data Distribution Service (DDS), a favorite candidate architecture for complex CPSs promoted by the Industrial Internet Consortium served as a testbed of the pilot prototype.