Brett Bicknell Karim Kanso

Advance

Verification and Validation of System Requirements by Animation and Automated Formal Analysis.

The emergent discipline of using formal modelling and analysis to support industrial scale requirements engineering has matured in recent years ^{[Woodcock et al. 2009]}. This article explores Event-B – one of the more well-developed methods within this field – by means of examples and comparisons to established methods. The Event-B method and Rodin toolset allow for modelling, animation and verification of system requirements (or parts thereof), and the toolset has been largely developed by EU framework projects, notably DEPLOY and ADVANCE.

Introduction

The ADVANCE project explores new ways of engineering cyber-physical systems ^{[Edmunds et al. 2012; Lee 2008]} that result in higher levels of assurances. Cyber-physical systems involve complex interactions between cyber and physical elements. For example, smart grids, robotics, and plant control systems are all cyber-physical systems. Typically, the cyber portions of the systems are the control systems and the physical portion is the environment. Previously, in issue 3 of the Requirements Engineering magazine, a general introduction to using the ADVANCE methodology to develop cyber-physical systems was published ^{[Bicknell et al. 2014]}. In summary, the previous article described a method where the cyber portions of the system and their requirements are modelled using the Event-B language, and the physical portions of the system are modelled using the Modelica language. These models are then co-simulated to validate the system requirements ^{[Blochwitz 2011]}. Further, due to the precise semantics of Event-B, the cyber models are amenable to advanced mathematical analysis to determine completeness, consistency and traceability of requirements – that is, performing formal verification.

Overview

This article is structured to provide a light introduction into the formal modelling discipline and Event-B language. Then, it explores the interface between natural language requirements and Event-B, and elaborates on using Event-B for cyber model development. The main body of the article describes, through a simple system example, how using the ADVANCE method and Event-B language improves the quality of requirements. Comparisons are also made with established approaches for the development of cyber-physical systems.

Event-B Overview

There are many different types of systems, each of which has an established method of design and development that is often domain specific. For example, the aviation, aerospace, automotive and medical industries all have their own well-established guidelines and accredited toolsets for system and software development. In contrast to this way of thinking, Event-B is a general purpose modelling language for systems that are event based. Digital systems are one class of system that Event-B is particularly well-suited to; this is because it is natural to abstract these systems to a level where only externally observed events are considered. For example, control actions that a system emits, or sensor inputs that the system receives, are events – after all, digital systems are ultimately discrete. Even in cases where sensor inputs are apparently continuous, there are boundary conditions or sample rates which correspond to events (essentially this is the foundation for fuzzy logic). Event-B has native support for non-determinism and asynchronism, and thus, it is not necessary to fully define the ordering and interrelationship of the events. In addition to observable events, Event-B also allows for the representation of the internal state of the system, which is used to define pre- and post-conditions on the events. That is, depending on the state of the system, different events are possible, and the effect of the event can also change depending on the state of the system. As an example, consider the traditional 4 variable model ^{[Parnas and Madey 1991]}, which fits into this methodology by translating the control actions and sensor telemetry into events, as highlighted in Figure 1.

The general strategy in Event-B is to create a system-level model, such as the one in Figure 1, consisting of abstract models of the control system and controlled process. Then, over time, these models are broken down and details are added into them. The important consideration at the high-level is to succinctly identify the events between the various system components.

The pre- and post-conditions on the events allow for the engineer to precisely, and unambiguously, define the behaviour of the system (i.e. order of events). But this mechanism does not ensure that the system is correct. To ensure correctness, system requirements are translated into Event-B invariants; see the next section for details on how this is achieved. Invariants are properties that the system must always fulfil. Using mathematical techniques, it is possible to determine whether the behaviour of the system fulfils these invariants, and hence the requirements.

The apt reader will have noticed that the above describes a general approach for abstractly modelling systems based on externally observable events. However, it does not consider internal events. Depending on the level of detail of the requirements being engineered, it might also be necessary to model internal system events, or similarly, identify emergent behaviour from composing sub-systems. To address this, there are two complementary methods provided for Event-B:

• Refinement: Details are iteratively added to models. This introduces more internal events, and augments existing event pre- and post-conditions. Using refinement builds up a more complete model of the system’s internal behaviour, and hence, reduces non-determinism in the system. This means that the system’s external behaviour becomes precise, and lower level requirements can be formulated. In addition, traceability between requirement tiers is provided naturally through the refinement approach.

• Decomposition: The system is broken down into its constituent parts, i.e. sub-systems. Each of these sub-systems is then treated in isolation. The decomposition method allows for a hierarchical approach to modelling the system, and is particularly powerful for identifying undesirable emergent behaviour of systems-of-systems. The hierarchical approach to modelling systems by decomposition is a common strategy, is used widely within SysML, and forms the basis of Model Based Design. However, when a system is decomposed there is the need to ensure that it still represents the whole system. Some toolsets check this automatically, however, they do not provide assurances about these checks. Using Event-B to perform this decomposition provides assurances. This stems from the fact that Event-B is a formal language, and the decomposition process is formal.

The refinement methodology is integral to effective use of Event-B. The engineer first provides a high-level view of the system, and then iteratively adds details into the model until the model is at a desired level of fidelity to represent the system and requirements – potentially this is all the way to a level of detail that is directly implementable. Whenever details are added, the engineer checks the model – with the support of automated tools – to ensure that they have not violated any requirements. This iterative approach facilitates incrementally verifying the system details against the requirements: First, the high-level system behaviour is checked against the system requirements then, as details are added, they are checked against these as well.

It is clear that using both refinement and decomposition provides the necessary meta-tools for requirements management. For example, consider the case of an aircraft on-board system. Following the initial safety analysis and system requirements definition, the system is decomposed into its constituent parts, including software and hardware. After decomposition, further refinements are performed to each of the decomposed components as per DO-178C and DO-254, which correspond to starting at high-level requirements and ending at low-level requirements, possibly through multiple intermediate layers.

Following the ADVANCE methodology and tools means that requirements are debugged early on in the system life-cycle, instead of identifying erroneous behaviour at later, more costly, phases of the life-cycle. Currently accepted methods of early requirements validation focus on the use of simulation toolsets and human experience. Some of the widely known and used toolsets for the early validation activities include MathWorks Simulink, Dymola, and Atego Modeller (formally Artisan Studio). These toolsets allow for the system to be modelled, in some cases with requirements linked to design elements, and then provide (possibly interactive) simulation of the system. However, these toolsets are based around the simulation tract, rather than the formal modelling and proof approach (some of these toolsets support limited formal analysis with add-on packages). This lack of a formal approach means that it is not canonical to ensure that requirements are consistent and free from undesirable behaviours. At best, simulation can only confirm the presence of erroneous behaviours, whereas formal methods unambiguously determine whether erroneous behaviours exist ^{[Malik and Khan 2013]}.

Within the formal modelling and proof tract, there are other languages and techniques besides Event-B and the Rodin toolset. One language that is gaining industrial acceptance is TLA+, which has been adopted by Amazon to verify the behaviour of complex algorithms ^{[Newcombe 2014]}. TLA+ and Event-B are very similar in nature; both are formal languages (based on set theory) and both are supported by tools that perform automated analysis. Where they differ is in their area of application; Event-B is well suited to high-level system engineering, whereas TLA+ is better suited to lower, implementation level, engineering. In part, this is because Event-B has good support (and emerging design patterns) in terms of refinement and decomposition. There are a plethora of other formal languages and techniques, however, most of these have not successfully been able to ascend to support requirements engineering activities, either because of a lack of automated analysis or limited expressibility of the modelling constructs.

Although not the subject of this article, it is possible to simulate Event-B models against environmental models to obtain the same style of validation that current methods provide. This includes the use of interactive visualisations, which can represent elements such as the system’s user interface, or rolled-up system views.

Natural Requirements to Event-B

There are three main issues that have limited the adoption of formal methods industrially: first is trusting the results of the formal analysis, such as getting the results accepted by a certifying authority, the second is the technical mathematical knowledge required to analyse the requirements, and finally, the third is bridging the gap between natural language and formal representation.

The third issue is a serious challenge. Formal representations are typically constructed using precise mathematical formulae, which can be analysed formally, but require experience to understand. Whereas natural language is not fixed, is very expressive and, as a result, often ambiguous. However, natural language is easier for humans to understand and thus is the choice language for writing requirements. Various approaches have been investigated to bridge this gap:

• Structured text: Sentences that match pre-determined lexicographic patterns. As these patterns are known in advance, they are easily translated into formal requirements. This is an intuitive approach as it is often the case that good requirements follow certain patterns, such as “the system shall …”, and avoid the use of vague words such as “should” and “appropriate”. However, the problem with restricting the engineer to certain constructs is that it almost always results in the engineer wanting to write requirements using patterns that have not been considered.
• Tractability: The engineer provides free form text representing the requirements, and then the requirements and their phenomena are linked to related model elements. This is a particularly expressive approach as it does not restrict the engineer, however, it does place an extra burden on the engineer to provide the top-level traceability between natural language and the formal models. After the initial tracing, traceability is managed automatically within the formal models.

The ADVANCE method follows the second approach, and places the responsibility on the engineer to map between natural language requirements and formal requirements. This is not ideal as there is (1) the possibility of human mistakes, and (2) dependency on the team creating the links to maintain and justify the traceability throughout the project. Even considering these issues, it aligns with current accepted practices. Rodin, the environment for developing Event-B models, is compatible with the requirements management tool ProR ^{[Jastram 2010]}. Using ProR, phenomena and requirements are defined using natural language and then, as the models are developed, parts of the models are linked to the ProR documents. The example in the following section describes this process.

Event-B Example

To better understand the benefits and limitations of using Event-B, and the associated Rodin toolset for requirements engineering, the development of requirements for an easily recognisable system – a clothes dryer – is considered.

Suppose that the dryer has the following top-level requirements:

[REQ-TL-1] The dryer shall only start if the door is closed and the door lock is locked
[REQ-TL-2] The door lock shall be locked whilst the dryer is on
[REQ-TL-3] The door lock shall be unlocked when the dryer is off

Event-B models are constructed of abstract state machines consisting of events and variables, where the events can change the state of variables. These state machines are described using set theory, and hence it is possible to unambiguously specify properties of the model. These properties are reflected as invariants in the Event-B model, and often represent the requirements of the system being modelled.

The state machine of the abstract system described by the top-level requirements above is shown in Figure 4, and the corresponding Event-B model is represented in Figure 5. The events in Figure 5 correspond to the transitions shown in Figure 4.

Each event has actions (listed under then) and guards (listed under where). The actions update the variables in the model, and the guards apply restrictions as to when the events can occur. Invariants are also included to specify the type of each variable in the model; for instance, the invariant dryer-type expresses that the variable dryer (which represents the abstract states of the dryer, as depicted in Figure 4) can take the values ON or OFF. There are additional variables in the Event-B model which track the state of the door and the lock.

The remaining invariants (inv1 and inv2) embody the requirements. The requirements are mapped to the Event-B model as follows:

• REQ-TL-1 is fulfilled by grd1 and act2 of the event Start
• REQ-TL-2 is translated into inv1
• REQ-TL-3 is translated into inv2

This link between the natural language requirements and the Event-B is recorded using the ProR plugin, as shown in the screenshot in Figure 6 below.

The elements in the Link column reflect the mapping specified in the bullets above (where M_abs corresponds to the Event-B model shown in Figure 5). The numbers before and after the arrows in the Link column indicate the number of elements the requirement is traced from and to respectively; the entries below this detail any downward traced elements. As these are top-level requirements, there is nothing above to trace to, so the initial number is zero in each case. This would not be the case for any derived requirements, as these would not only be traced to the Event-B model, but also traced upwards to the top-level requirements. The tool facilitates linking between different requirement sets as well as between requirements and the formal models. Also, note how elements in the Event-B model can be referred to directly in the requirements, such as the event Start or the states CLOSED and LOCKED; this can help clarify the transition from natural language to Event-B.

Any changes to either the requirements or models will be highlighted by the tool, in which case the link will need to be re-validated to ensure no consistency has been lost. An example of this can be seen in the Target column in Figure 6; the warning symbol indicates that the target of the link – the Event-B element – has been modified.

Consistency and Correctness

When the model is created proof obligations are automatically generated, which need to be proven in order to demonstrate the model elements are consistent and, in the case of invariants, always hold. Automatic proof tools are available in Rodin to assist with this, although it may still be necessary to provide manual proof steps to help the automated provers along when dealing with more complex proof obligations. For the model in Figure 5, all of the proof obligations were proven automatically, showing that the invariants hold for the reachable state space of the state machine in Figure 4. This is not too surprising, as the model is fairly simple. To demonstrate some more interesting analysis, some derived requirements for the dryer will be introduced.

We will consider that the operation of the dryer is controlled through a combination of a switch and humidity sensor. It is possible to manually start and stop the dryer through the switch, but the dryer will also automatically turn off if it detects that the clothes are dry. This could correspond to introducing the following derived requirements:

[REQ-DRV-1] The dryer shall turn on when the switch is turned on
[REQ-DRV-2] It shall only be possible to turn the switch on if the door is closed and locked
[REQ-DRV-3] The dryer shall stop when the switch is turned off
[REQ-DRV-4] The dryer shall have a humidity sensor which provides a low or high output
[REQ-DRV-5] On dryer start, the humidity sensor shall provide a high output
[REQ-DRV-6] The dryer shall stop when the humidity sensor provides a low output
[REQ-DRV-7] The door shall be locked when the switch is turned on
[REQ-DRV-8] The door shall be unlocked when the switch is turned off

To introduce this additional detail, we first decompose the Event-B model into separate parts for the control and humidity sensor sub-systems, and then further refine the control sub-system to add the derived requirements. This approach is depicted in Figure 7 below. For the sake of this example, we will focus on the resulting control sub-system model, and demonstrate how it helps analyse the consistency and completeness of the derived requirements. However, the refinement technique is set out so that development could also be continued on the humidity sensor sub-system separately.

The state machine of the resulting control sub-system model, which includes the behaviour introduced by the derived requirements, is shown in Figure 8. This state machine refines that introduced earlier in Figure 4 - the abstract states and transitions from Figure 4 are shown in grey above the refined states and transitions of the new state machine.

The Event-B model which corresponds to this refined state machine is shown in Figure 9; the translation from the state machine to the Event-B is explained in steps below.

During Event-B refinement it is possible to add new variables and events. In the control sub-system model, two new variables have been added; switch and sensor. These represent the state of the switch and the output of the sensor respectively. The variable dryer from the abstract model has also been removed; this is because the abstract notion of the dryer being on or off has been replaced by the more concrete notions of the switch and sensor. The relationship between the abstract and concrete states in Figure 8 is reflected in the invariants gluing-1 and gluing-2 in the Event-B model. These invariants provide the ‘gluing’ between the abstract and concrete variables.

It is also possible to refine existing events, either by adding new guards and actions, or replacing existing guards and actions with more concrete implementations. The event SwitchOn refines the abstract event Start using both of these techniques. In this event, grd1 and act2 have been carried over from the abstract model. However, grd2 has been added, and act3 and act4 replace the more abstract action act1. Note that it is also possible for more than one concrete event to refine a single abstract event; both SwitchOff and ReadSensor_Low refine Stop, representing the fact that the derived requirements specify more than one way in which the dryer can be stopped. The events OpenDoor and CloseDoor remain the same in the refinement.

The link between the control and humidity sensor sub-systems is introduced through the ReadSensor event. This has been split into two separate events in the control sub-system model – ReadSensor_Low and ReadSensor_High – due to the fact that different actions will occur depending on the output value of the sensor. The dryer should only stop if the output value is low; hence ReadSensor_Low refines Stop but ReadSensor_High does not. A parameter – val – is passed into the ReadSensor events, which represents the output of the sensor passed to the control sub-system. The implementation of what value this parameter should take at any point in time is specified in the humidity sensor sub-system, which ‘shares’ this event.

The traceability between the derived requirements and the refined Event-B model is as follows:

• REQ-DRV-1 (The dryer shall turn on when the switch is turned on) is fulfilled by the fact that SwitchOn refines Start
• REQ-DRV-2 (It shall only be possible to turn the switch on if the door is closed and locked) is fulfilled by grd1 and act2 in the event SwitchOn
• REQ-DRV-3 (The dryer shall stop when the switch is turned off) and REQ-DRV-6 (The dryer shall stop when the humidity sensor provides a low output) are represented by the invariant gluing-2
• REQ-DRV-4 (The dryer shall have a humidity sensor which provides a low or high output) is represented by the addition of the variable sensor and the input val of the ReadSensor events
• REQ-DRV-5 (On dryer start, the humidity sensor shall provide a high output) is fulfilled by act4 of the event SwitchOn
• REQ-DRV-7 (The door shall be locked when the switch is turned on) is translated into inv3
• REQ-DRV-8 (The door shall be unlocked when the switch is turned off) is translated into inv4

You will notice that requirements can also be associated with guards, actions, and even variables if applicable.

As the refinement in the Event-B model is formal, the proof obligations that are automatically generated through the refinement can tell us if the derived requirements are consistent and complete – not only amongst themselves, but also against the top level requirements. This is due to the fact that proof obligations are not only generated for the new invariants, but also for any refined events. The latter ensures that the traceability between the different models is maintained.

In the new set of proof obligations for the model in Figure 9, it is not possible to prove that the refinement of ReadSensor_Low is consistent, nor is it possible to prove that the invariant gluing-1 is maintained. After some inspection the reason for this is apparent; in the current iteration a low value from the humidity sensor can stop the dryer, but the switch remains on. As gluing-1 provides the ‘gluing’ between the abstract and concrete variables, the difficulty proving this represents an inconsistency between the top level and derived requirements. In particular, that REQ-TL-3 is not fulfilled by the derived requirements, as the dryer can be ‘off‘ from the perspective of the top level requirements, but the door remains locked (because the switch is still on). By changing the event ReadSensor_Low to the following, all of the proof obligations can be successfully proven:

The addition of act4 corresponds to a missing derived requirement: When the humidity sensor provides a low output, the switch shall automatically be turned off. The door is also unlocked at the same time – act5 – to fulfil REQ-DRV-8. Thus it is possible not only for the modelling to highlight inconsistencies, but also point towards missing requirements.

Although this is quite a simplistic example, Event-B is not limited to simple sets, assignments and conditions. More complex behaviour can be represented through set operations on functions, relations or natural numbers, and invariants or guards can include quantifiers, i.e. for all (∀) and for each (∃).

Conclusion

This article has explored Event-B and the ADVANCE method for systems engineering through an example of a clothes dryer. The example covered linking natural language requirements to model elements and the formal development of the solution, using both decomposition and refinement. In addition, the example illustrated how to debug the requirements, by using the automated tools to identify an erroneous behaviour.

The ADVANCE method is most applicable to modelling event based systems, such as embedded controllers, communications protocols and cyber-physical systems. In principle, it could be applied to non-digital systems, provided they are event driven, such as business processes or cellular biology, however, these are beyond the scope of the ADVANCE project. The technical underpinnings of the Event-B toolset are well suited to analysing discrete control or software systems, however, analysing continuous aspects of these systems is harder to achieve as the toolset is less suited or matured in these areas. As a result, it is difficult to express performance properties, such as timing or continuous physical behaviour. It is for this reason that the ADVANCE framework allows for the Event-B models to be simulated in step with external, continuous models, where these properties can be more naturally expressed. This co-simulation of the models is covered in more detail in our previous article ^{[Bicknell et al. 2014]}.

The toolsets and methodology developed within ADVANCE reduce the long standing barriers that have inhibited the serious adoption of such methods within industry. These include the use of the ProR plugin to link natural language requirements to their formal counterparts, and automated tools that analyse the models. The ProR traces provide invaluable information that eases the verification and validation (V&V) process when the requirements are represented as mathematical formulae. Automated analysis of the models reduces the burden of mathematical knowledge on the engineers – formal proofs are not carried out manually. In addition, these tools increase productivity due to the reduced work load on the engineering team.

There is a down side: when using automated tools for checking traceability and consistency of requirements, there are scalability issues; that is, when the models become large, the tools fail to terminate within a reasonable time and require substantial processing resources. Careful use of refinement and decomposition ensures that at each step the models do not become too large, and hence, increases the feasibility of automated analysis for larger systems, however, there is still a limit. The precise limit is not known, and is highly dependent upon the structure of the models, automated tools in use, and computing resources available. It is often the case that models need to be restructured to take full advantages of speedups within the underling automated tools – this is where experience and technical support from the toolset developers is invaluable. Yet, the ADVANCE framework has been used to support the development of a variety of large complicated systems, including: smart grids, train interlocking systems, satellite flight formation algorithms, and processor architectures. As a result of these studies, it is evident that the technique of incremental model development is emerging to be as important for software development as producing well-structured and manageable code.

As the appetite for these formal techniques is wetted within industry, as reflected by new standards governing their use, questions and realisations about how they affect later parts of the system life-cycle are being raised. One realisation pertains to V&V: The V&V engineer will need an understanding of formal techniques, how they were applied, and the semantics of the traceability information, in order to understand whether the evidence provided is sufficient.

Following the ADVANCE methodology and tools means that requirements are debugged during system design and development. In our experience, applying the ADVANCE methodology early on in the system’s life-cycle provides the greatest benefits. These include the identification of:

• Subtle undesirable behaviours,
• Inconsistent requirements,
• Unsatisfied requirements.

Predictably, there is a trade-off as the time and effort to develop the requirements is increased. However, not only does the approach reduce the cost later on in the system life-cycle, it also provides a higher level of assurance overall, on both the requirements and design.

References

• [1] Abrial, J.-R., Modeling in Event-B: system and software engineering. UK:Cambridge University Press, 2010.
• [2] Abrial, J.-R. et al., Rodin: an open toolset for modelling and reasoning in Event-B. International Journal on Software Tools for Technology Transfer. volume 12:447-466, 2010.
• [3] Bicknell, B., Kanso, K. and McLeod, D., ADVANCE: A New Approach for Requirements Validation and Rigorous Verification. IREB, 2014.
• [4] Blochwitz, T. et al., The Functional Mockup Interface for Tool independent Exchange of Simulation Models. In proceedings of 8th Modelica Conference, Dresden, Germany, 2011.
• [5] Edmunds, A., Colley, J. and Butler, M., Building on the DEPLOY legacy: code generation and simulation. DS-Event-B-2012: Workshop on the experience of and advances in developing dependable systems in Event-B, 2012.
• [6] Fritzson, P., Principles of object-oriented modeling and simulation with Modelica 2.1. John Wiley & Sons, 2010.
• [7] Jastram, M., ProR, an Open Source Platform for Requirements Engineering based on RIF. In proceedings of Systems Engineering Infrastructure Conference, Munich, Germany, 2010.
• [8] Lee, E., Cyber Physical Systems: Design Challenges. University of California, Berkeley Technical Report No. UCB/EECS-2008-8, 2008.
• [9] Leuschel, M. and Butler, M., ProB: A Model Checker for B. Lecture Notes in Computer Science. Volume 2805:855-874, 2003.
• [10] Malik, S. and Khan, S., Formal methods in Large Scale computing systems. BCS, 2013.
• [11] Newcombe, C. Why Amazon Chose TLA+. Lecture Note in Computer Science. volume 8477:25-39, 2014.
• [12] Parnas, D. and Madey, J., Functional Documentation for Computer Systems Engineering, Vol. 2, McMaster University, Hamilton, Ontario, Technical Report CRL 237, 1991.
• [13] Savicks, V., Butler, M., Bendisposto, J., and Colley, J., 2013. Co-simulation of Event-B and Continuous Models in Rodin. Proceedings of 4th Rodin User and Developer Workshop. June, Turku, Finland.
• [14] Snook, C., Butler, M., 2006. UML-B: Formal modeling and design aided by UML. ACM Transactions on Software Engineering and Methodology volume 15 issue 1:92-122.
• [15] Woodcock, J., et al., 2009. Formal Methods: Practice and Experience. ACM Computing Surveys volume 41 issue 4:1-40.