Requirements Modelling for Cyber-Physical Systems

Cyber-physical systems (CPSs) are characterised as systems that are controlled and monitored by software and are tightly integrated with the internet and its users. Physical and software components are intimately linked, operating in different time-bands and at different spatial scales. They exhibit emergent behaviours arising from their interactions and changing environments. Examples of CPSs include smart grids, self-driving cars, fly-by-wire avionics, personalised healthcare, process control systems, and autonomous robotics. CPSs are complex and raise significant challenges in dependability and trust. Correspondingly strong guarantees are needed in order to justify their deployment. This project addresses these issues by devising and supporting methods for modelling their requirements and providing precise contracts for what a CPS may and may not do.

We propose the use of contracts to specify local functionality, interactions between components, and component behaviours. In York, we will increase the guarantees that can be made using a popular industrial tool, a graphical programming environment for modelling, simulating and analysing multi-domain dynamic systems.

Simulink is a widely used industrial language and tool-set for expressing control-law diagrams, including support for simulation and code generation. Though empirical analysis through simulation is an important technique to explore and refine models, only formal verification can make specific mathematical guarantees about behaviour, which is crucial to ensure safety of associated implementations. Whilst verification facilities for Simulink exist [1, 17, 16, 13], there is still a need for assertional reasoning techniques that capture the full range of specifiable behaviour, provide nondeterministic specification constructs, and support compositional verification. Such techniques also need to be sufficiently expressive to handle the wide variety of additional languages and modelling notations that are used by industry in concert with Simulink, in order to allow formulation of heterogeneous multi-models that capture the different paradigms and disciplines used in large-scale systems [18]. Applicable tool support for these techniques with a high degree of automation is also of vital importance to enable adoption by industry. Since Simulink diagrams are rich in data and usually have an uncountably infinite state space, model checking alone is insufficient and there is a need for theorem proving facilities.

Assume-Guarantee (AG) reasoning is a valuable compositional verification technique for reactive systems [14, 11, 2]. In AG, one demonstrates composite system-level properties by decomposing them into a number of contracts for each component subsystem. Each contract specifies the guarantees that the subsystem will make about its behaviour, under certain specified assumptions of the subsystem’s environment. Such a decomposition is vital in order to make verification of a complex system tractable, and to allow development of subsystems by separate teams. AG reasoning has previously been applied to verification of discrete time Simulink control-law diagrams through mappings into synchronous languages like Lustre [3] and Kahn Process Networks [16]. However, such formalisms, whilst theoretically and practically appealing, are limited to expressing processes that are inherently deterministic and non-terminating in nature. This can be addressed by translating to several additional notations where AG verification can be performed; but this hampers both traceability and composition with other languages of different paradigms. What is needed is a rich unified language capable of AG reasoning, and supported by theorem proving, into which Simulink and associated notations can be faithfully translated.

We are exploring the development of formal AG-based proof support for discrete-time Simulink diagrams through a semantic embedding of the Circus language [15] in Isabelle/HOL. Circus is a formal modelling language for concurrent reactive systems in the style of Hoare’s CSP, but with support for modelling mutable state variables. A Circus model consists of a network of processes that communicate with one another solely via shared channels that carry typed data. Internal state variables are encapsulated and not directly observable by other parallel processes. Circus can capture a variety of languages at the semantic level, supporting the formulation of heterogeneous multi-models by acting as a lingua franca [18]. Previous work at York has used Circus to give a semantics to discrete-time Simulink diagrams [4]. The semantics uses processes to model blocks and channels to model wires. It has previously been used to define a refinement strategy from Simulink control laws to concurrent implementations [5]. A number of supporting tools exist, including ClawZ [1], which allows formal verification of sequential code against a Simulink diagram, and also a mechanised translation from Simulink model files to Circus [12]. As yet, there are no theorem proving facilities for the Circus Simulink models, and these we are proposing to develop, based on the Isabelle theorem prover.

Circus has a denotational semantics in Hoare and He’s Unifying Theories of Programming [10, 6] (UTP). Over the past five years, we have been working on an Isabelle-based proof environment called Isabelle/UTP [9]. This allows us to the encode semantic meta-models for programming and modelling languages, prove fundamental algebraic laws, formalise meta-model links, construct tactics to automate proof, and finally subject concrete models to verification and analysis via theorem proving. Isabelle/UTP has a prototype implementation of Circus, which we will develop further during this project.

Recently, we have extended Circus with a contract notation for AG-style reasoning. It allows us to specify contracts for hardware or software components over state variables and a trace of the system’s behaviour up to the point of the contract. The contract includes three components: the first (the precondition) specifies the assumptions that can be made for the validity of the contract; the second (the peri-condition) guarantees to the user of the contract how the component will behave during its operation; the third (the postcondition) guarantees the final outcome of executing the component. It should be noted that the precondition actually does double duty. As the contract must be in force during the component’s execution, it also describes assumptions on the behaviour of the component’s environment during this execution.

We have been developing a rich algebra for the composition of contracts in different architectural combinations. The laws are supported by weakest precondition-style operators that characterise, for example, the weakest reactive assumption a process may make about its environment. Significantly, our contracts have a natural notion of refinement, weakening preconditions and strengthening peri- and postconditions.

Our contract notion is not limited to discrete states and traces, but applies also to a semantics involving piecewise continuous functions [7]. In the future, we envisage this supporting continuous and hybrid Simulink diagrams. Our techniques are general and may be applied to other languages, such as rCOS and industrial standards, such as Modelica [8].

Tasks

We propose a close collaboration with our Chinese colleagues in Chongqing. We want to establish a programme of research that will lead to a theory of model- driven cyber-physical architecture. This will be founded on the theory of AG contracts that we have been building in our Isabelle theorem prover. SWU will lead the development of the theory at the architectural level. This will involve modelling both components and their compositions of subsystems of diverse software functions with embedded hardware, instantiating raw physical processes (or plants). They will also work on augmenting the architecture with intelligent computational components that coordinate and manage the operations of the system. Architectural modelling will be based around the notion of interaction contracts.

The York team will undertake the following tasks.

1. We will continue our mechanisation of Simulink semantics in Isabelle/UTP, including a selection of discrete blocks from the Simulink library as Circus processes. The selection will be chosen based on the project’s case studies.

2. We will develop a mechanised library of examples, again based on the project’s case studies, together with contracts and proofs of correctness. We will make use of the library of publicly available case study materials produced by the EU H2020 INTO-CPS project (of which York is a participant) in the domains of railways, smart buildings, automotive, and agriculture.

3. Based on the examples, we will automate techniques for reasoning about interferences between blocks and subsystems. This will be supported by proof tactics that will allow us to demonstrate how a subsystem’s behaviour is contingent on its context. We will also explore more general verification techniques through contractual refinement.

4. Jointly with SWU, we will conduct requirements modelling and analysis on case studies to assess the feasibility of the modelling approach and the tool support. The case studies will be (i) a Smart Home System already studied in a project between SWU and Aalborg University; and (ii) robotics and railway systems taken from the INTO-CPS project.

References

[1] R. Arthan, P. Caseley, C. O’Halloran, and A. Smith. ClawZ: Control laws in Z. In Proc. 3rd Intl. Conf. on Formal Engineering Methods (ICFEM), pages 169–176. IEEE, September 2000.

[2] S. Bauer, A. David, R. Hennicker, K. Larsen, A. Legay, U. Nyman, and A. Wasowski. Moving from specifications to contracts in component-based design. In FASE, volume 7212 of LNCS, pages 43–58. Springer, 2012.

[3] P. Caspi, A. Curic, A. Maignan, C. Sofronis, and S. Tripakis. Translating discrete-time Simulink to Lustre. In EMSOFT, volume 2855 of LNCS, pages 84–99. Springer, 2003.

[4] A. Cavalcanti, P. Clayton, and C. O’Halloran. Control law diagrams in Circus. In 13th. Intl. Symp. on Formal Methods (FM), volume 3582 of LNCS, pages 253–268. Springer, 2005.

[5] A. Cavalcanti, P. Clayton, and C. O’Halloran. From control law diagrams to Ada via Circus. Formal Aspects of Computing, 23(4):465–512, Jul 2011.

[6] A. Cavalcanti and J. Woodcock. A tutorial introduction to CSP in unifying theories of programming. In Refinement Techniques in Software Engineering, volume 3167 of LNCS, pages 220–268. Springer, 2006.

[7] S. Foster, A. Cavalcanti, J. Woodcock, and F. Zeyda. Unifying theories of time with generalised reactive processes. Submitted to Information Processing Letters, May 2017.

[8] S. Foster, B. Thiele, A. Cavalcanti, and J. Woodcock. Towards a UTP semantics for Modelica. In UTP, volume 10134 of LNCS. Springer, June 2016.

[9] S. Foster, F. Zeyda, and J. Woodcock. Unifying heterogeneous state-spaces with lenses. In ICTAC, volume 9965 of LNCS. Springer, 2016.

[10] T. Hoare and J. He. Unifying Theories of Programming. Prentice-Hall, 1998.

[11] C. B. Jones. Wanted: a compositional approach to concurrency. In Programming Methodology, Monographs in Computer Science, pages 5–15. Springer, 2003.

[12] C. Marriott, F. Zeyda, and A. Cavalcanti. A tool chain for the automatic generation of Circus specifications of Simulink diagrams. In ABZ, volume 7316 of LNCS. Springer, 2012.

[13] MathWorks. Simulink Design Verifier. mathworks.com/products/sldesignverifier.html.

[14] B. Meyer. Applying “design by contract”. IEEE Computer, 25(10):40–51, 1992.

[15] M. Oliveira, A. Cavalcanti, and J. Woodcock. A UTP semantics for Circus. Formal Aspects of Computing, 21:3–32, 2009.

[16] Boström P. and J. Wiik. Contract-based verification of discrete-time multi-rate Simulink models. Software and Systems Modelling, 15:1141–1161, 2016.

[17] P. Roy and N. Shankar. SimCheck: A contract type system for Simulink. Innovations in Systems and Software Engineering, 7:73–83, 2011.

[18] F. Zeyda, J. Ouy, S. Foster, and A. Cavalcanti. Formalised cosimulation models. In Proc. 1st Workshop on Formal Co-Simulation of Cyber-Physical Systems, LNCS. Springer, 2017.