Formal methods are widely recognized as powerful engineering methods for the specification, simulation, development, and verification of embedded systems [BS01]. They follow the principle of "correctness by construction" and are therefore well suited for safetycritical systems [HC02]. Although the advantages of formal methods are well known [LG97], there are many limitations preventing their usage in industrial systems.
The industrial systems evolve to more and more complex structures to meet the increasing complexity of requirements, especially when combining embedded systems with physical components, termed Cyber-Physical Systems (CPSs). Moreover, the involvement of multiple engineering disciplines, which are targeting cross cutting aspects of the system under development, facilitates wider application of formal methods, which can overcome the underlying challenges. In particular, the pursuit of shorter development time and smaller project budgets requires: 1) an increased parallelization of the single development steps 2) consistent exchange of information between the involved disciplines 3) a strategy for the validation of functional requirements at an early stage. Thus, flexible and efficient modelling frameworks are required which should include more powerful engineering tools and methods. Such a modelling framework has been developed within the German research project SPES XT1 [PHAB12], which on the one hand facilitates reuse and allows an efficient artefacts development while on the other hand it is designed to be independent of any application domain. In doing so, we apply the SPES methodology to a case study from the automation domain, focusing on the control software components of a desalination plant. This paper is structured as follows: Section 2 presents the related foundations w.r.t. the system model, the development method and tool support required for the case study. Section 3 illustrates the set-up of a case study of a desalination plant which is modelled according to a formal system model FOCUS and the SPES development method. Furthermore, the verification of functional requirements is addressed. Section 4, discusses the benefits of a model-based development approach. Finally, Section 5 concludes the present work and describes possible future directions.
We perform this case study based on the formal system model FOCUS [BS01], the modelbased development method SPES[BDH + 12], as well as the CASE tool AutoFOCUS 3 which supports both the formal system model as well as the development method.
The system model FOCUS (for details, see [BS01]) is based on a specific notion of a system. A system is represented as a model consisting of a syntactic interface, denoting the input and output channels. Through the channels the system can communicate with its environment. The behavior of the system can be observed at the interface.
Formally, we can represent a syntactic interface as a pair I ⊲ O, where I is a set of input channels and O is a set of output channels. We can represent the behaviour of a system as a function
Here, C ∞ denotes an infinite sequence of messages for every channel in the channel set C. Using this notion of a system and its behaviour, we can compose systems from subsystems. Formally, we can define the composition S 1 ⊗ S 2 for two interface behaviours S 1 and S 2 representing the behaviour of the subsystems.
In the research project SPES, the SPES Modelling Framework (SPES MF) is developed to enable seamless model based development for embedded systems [BDH + 12]. The SPES MF focuses on artefacts that are created during the development of embedded systems and structures artefacts according to viewpoints. The SPES MF differentiates between the following four viewpoints:
• Requirements Viewpoint: structured documentation and analysis of requirements • Functional Viewpoint: structured documentation and analysis of system functions and their behaviour (Functional Architecture) • Logical Viewpoint: structured documentation and analysis of the logical solution (Logical Architecture) • Technical Viewpoint: structured documentation and analysis of the technical solution (Technical Architecture).
To further reduce the complexity of the engineering process, the SPES MF introduces layers of granularity, where a coarse-grained engineering problem is decomposed into a number of more fine-grained engineering problems following the principle "divide and conquer", i.e. the composition of the fine-grained solutions is a solution for the coarsegrained engineering problem. Whenever a coarse-grained engineering subject is decomposed into a number of fine-grained engineering subjects, a new layer of granularity is constructed. Hereby, the system is decomposed into smaller and less complex parts. Since the number of such layers depends on the properties of the individual engineering context of an embedded system, the SPES MF does not define a fixed number of granularity layers. Most artefacts that are included within the SPES MF can formally be described using the formal system model outlined above.
AutoFOCUS 3 [HF11] is an open source research tool supporting model-based development, formal specification and analysis, as well as design space exploration techniques2 . It provides a broad range of modelling concepts at different levels of formalization for different phases in the development ranging from requirements (using the AutoFOCUS 3 plugin MIRA [TMR13]) to platform architecture and deployment. Specifically, it provides support for most of the modelling artefacts described in the SPES MF.
Yet today, 780 million people live in lands where there is a lack access to potable water. The production of drinking water by desalination of sea water represents a way to reduce the lack of clean water. In the following we consider a typical desalination plant with reverse osmosis (See Figure 1). The general principle of desalination plant with reverse osmosis is the following.
Water is collected by four beach wells along the coast. The salt water is then pumped into the seawater tank, where it is collected. After pretreating with various chemicals for stabilization and biochemical cleaning the actual desalination process can take place. Therefore the water passes several filters before separating the salt in the high pressure section. After post treatment new drinking water can be delivered into the water net. This type of plant usually is of middle to high automation complexity. As the entire desalination plant is very complex, therefore for plausibility we consider only a small part of the Beach Well-section (BWS).
The main function of BWS in a desalination plant is pumping seawater from the sea to the sea water tank. This water is filtered by natural layers of sand. In order to guarantee sufficient water to operate this desalination plant, the level of the seawater tank should be monitored and controlled by switching pump valves.
We start our proposed seamless and continuous design approach by system requirement modelling of BWS. To provide artefacts of the system like glossary, use cases description, architectural constraints, and external environment of the system, MIRA is used in this phase to elicit, specify and analyse requirements. For instance, to avoid wrong interpretation we defined all relevant technical terms by building a glossary.
To formalize the textual requirements we propose to categorize requirement. In this example, all requirements are categorized into two categories according to the component to which they deploy: Beach Well (BW) and Beach Well Automation (BA).
Then each requirement is specified in text form and analysed as an use case. The requirement analysis is integrated with architecture design, since the component interface is derived by the relevant use cases specification which describes the components and the interactions between them. As shown in Fig. 4, the partial interface of a component can be derived from the BW4 use case description of the component Beach Well. Requirement BW4 has two input ports (FB Closed and FB Open, which indicate the feedback of pump to mark if discharge valve is closed or open) and two output ports (QON and QOFF which determine pump motor's work state is on or off). In this example, all i/o ports are Boolean-valued.
To avoid the consistency and ambiguity problems, the informal requirements should be modelled formally with structured text templates but still in a use-friendly textual manner. Fig. 5 illustrates the Assumption/Guarantee (A/G) specification of requirement BW4. Thus, requirements for completeness, correctness, and consistency can be later analysed with a model checker (cf. Sec. 3.4). Thereby, verification is possible in the early stage of requirement modelling process.
A functional architecture of the system is derived from the requirement artefacts according to the presented SPES development method. This view is focused on the behaviour of the system, i.e. on functionalities and features. Moreover, it represents also a sort of documentation of the system to be developed. Functions can be subdivided in sub-functions and relations can be structured between them.
We constructed a functional representation of the system in AutoFOCUS 3 using component architectures. Each component has a formal defined interface through i/o ports and an internal behaviour. We defined a root component that represents the whole functional architecture. We subdivided the requirements in two categories: requirements relative to the control of the whole plant and to a single beach well element. Therefore, we model each requirement category as a subcomponent, which is contained in the root component of the functional architecture. The i/o ports of these components are derived directly from the relative requirement artefacts. In fact, the functional specifications of the requirements permit to define the typed i/o interface of the functional architecture components.
We decided to implement the internal behaviour of each component with a finite state machine. There are also other alternatives, as for instance functional and code specifications. In Figure 6 the components corresponding to the requirement categories are depicted and the state machine implementing the single beach well functionalities is represented. This implementation has only the states and transitions relevant for the presented BW4 requirement. State machines can be simulated with desired environment conditions and can be formally verified as explained in the next section.
The definition of a functional architecture of the system permits to detect inconsistent and incomplete requirements using simulation and verification techniques. That is possible with enough detailed definition of the requirements with informal and formal artefacts. In our case study, we modelled formally each requirement through verification patterns, which permits the formal verification of its validity through the NuSMV4 model checker. Model checking offers an automatic and exhaustive proof of the system. The patterns are used for the presentation, codification and reuse of formal properties for AutoFOCUS 3 models. We associate verification patterns from the requirement to the functional architecture with refinement rules, which define a correspondence between the i/o ports of the formalized requirements and the functional architecture.
The verification patterns integrated in the AutoFOCUS 3 model view are of two types: patterns based on the specification patterns presented in [DAC99] and specifications conceived for AutoFOCUS 3 model. Further information about the specification of properties and the model checking integration in AutoFOCUS 3 are in [CHN11]. A verification pattern represents common and recurrent properties, as for instance a state or event of the system that must be reached after a state or event has happened. They are saved with the verification results along with the model itself. Each pattern is structured in a predefined logical part of the property, which determines its semantics and text fields to be filled. Typically, the user writes in these fields expressions that correspond to states, events, or port values and logical operators to combine them. When the pattern is completed an automatic type and name check is made to prove the correctness of the information inserted. Short descriptions help the user to understand the role of each text field.
A verification context has to be specified, in terms of components to be considered, to execute the verification. Then the tool translates the property to a formal logical property and the AutoFOCUS 3 model to an input model for NuSMV and executes it. A counterexample is reported if the result of the verification is negative. A counterexample may represent in the state machine either a path from the initial state to an erroneous state or a loop, where a desired behaviour never happens. Each step of the counterexample sequence is described by the actual value of variables and i/o ports of the verified model. The counterexample can be stepwise simulated in a graphical view of the tool to debug the AutoFOCUS 3 model. In each simulation step the variables and i/o ports values are visualized. The verification of the requirements in the functional architecture and the counterexample simulation are shown in Figure 7.
In the presented case study we formally verified requirements over the system behaviour expressed in the functional architecture. We studied a seamless model integration between requirements, formal properties definition, model checking and counterexample simulation. AutoFOCUS 3 provided a suitable environment to apply these concepts to our automation case study of beach wells. Our verification approach in the early development phases allows to avoid errors and incomplete requirements that can be much more expensive, if detected in successive development phases. In the requirements definition and elicitation phases, we specified for each requirement a typed i/o interface in a functional specification and we formalized behaviours in logical formulas expressed in verification patterns. These specifications make the requirements much more precise and with a defined semantics, in comparison with textual informal or semi-formal requirements descriptions. Furthermore, we verified and executed counterexample analysis without requirements of specific skills in formal verification.
Besides erroneous behaviour and incompleteness, the definition of dependencies between functions helps to solve interaction conflicts. Moreover, there is an improvement in the communication between experts of different disciplines, which are normally involved in the development of automation software. In fact, functional descriptions do not require all implementation details in contrast to the following logical and technical representations of the system. In these representations the functions modelled in the functional architecture are refined. Our verification approach proofs the system in a representation that abstracts from many details. Some of them are specific for a certain discipline. Therefore, we have an executable and verifiable system representation in a sort of discipline neutral language.
In this paper we investigated the application of the SPES development method for the automation domain. In particular, a case example of a seawater desalination plant was modelled according to that method. Special emphasis was given to the verification of functional requirements at an early stage of the development process. Moreover, AutoFOCUS 3 permits to model the successive logical and technical representations of the system. Thus, the intention of this paper was to provide an example in order to exhibit the additional value provided by SPES development method in the automation domain. Last but not least, possible future direction will be to explore the scalability of our approach, how to integrate real-time aspects and how deployment of these verified models to the engineering tools and the hardware used in the automation domain is possible. This gives a chance to transfer know-how to other application domains such as the smart grid domain and the execution of custom case studies within these domains.
* This work was partially funded by the German Federal Ministry of Education and Research (BMBF), grant "SPES XT, 01IS12005M". The responsibility for this article lies with the authors.