Inferring physical units in formal models

Most state-based formal methods, like B, Event-B or Z, provide support for static typing. However, these methods and the associated tools lack support for annotating variables with (physical) units of measurement. There is thus no obvious way to reason about correct or incorrect usage of such units. We present a technique that analyzes the usage of physical units throughout B and Event-B machines infers missing units and notifies the user of incorrectly handled units. The technique combines abstract interpretation with classical animation, constraint solving and model checking and has been integrated into the ProB validation tool, both for classical B and for Event-B. It provides source-level feedback about errors detected in the models. We also describe how to extend our approach to TLA \(^+\), an untyped formal language. We provide an in-depth empirical evaluation and demonstrate that our technique scales up to real-life industrial models.     

Derivation of concurrent programs by stepwise scheduling of Event-B models

Concurrent programs are often complex and they are not straightforward to develop and prove correct. Formal development methods based on refinement make it possible not only to derive programs gradually, but also to prove their correctness in a stepwise fashion. Event-B is a formal framework that has been shown useful for developing concurrent and distributed programs. In order to scale to large systems, models can be decomposed into sub-models that can be refined semi-independently and executed in parallel. In this paper, we show how to introduce explicit control flow for the concurrent sub-models in the form of event schedules. The purpose of these schedules is both to provide process-oriented specifications of the programs to complement the state-based approach in Event-B, as well as to facilitate more efficient implementation of the models. The schedules are introduced in a stepwise manner and should be designed to result in a correctness-preserving refinement step. In order to reduce the verification burden on the developers, we provide patterns for schedule introduction, together with their associated proof obligations. We demonstrate our method by applying it on the dining philosophers problem.     

A formal approach for the development of reactive systems

Context

This paper deals with the development and verification of liveness properties on reactive systems using the Event-B method. By considering the limitation of the Event-B method to invariance properties, we propose to apply the language TLA⁺ to verify liveness properties on Event-B models.

Objective

This paper deals with the use of two verification approaches: theorem proving and model-checking, in the construction and verification of safe reactive systems. The theorem prover concerned is part of the Click_n_Prove tool associated to the Event-B method and the model checker is TLC for TLA⁺ models.

Method

To verify liveness properties on Event-B systems, we extend first the expressivity and the semantics of a B model (called temporal B model) to deal with the specification of fairness and eventuality properties. Second, we propose semantics of the extension over traces, in the same spirit as TLA⁺ does. Third, we give verification rules in the axiomatic way of the Event-B method. Finally, we give transformation rules from a temporal B model into a TLA⁺ module. We present in particular, our prototype system called B2TLA⁺, that we have developed to support this transformation; then we can verify liveness properties thanks to the model checker TLC on finite state systems. For the verification of infinite-state systems, we propose the use of the predicate diagrams and its associated tool DIXIT. As the B refinement preserves invariance properties through refinement steps, we propose some rules to get the preservation of liveness properties by the B refinement.

Results

The proposed approach is applied for the development of some reactive systems examples and our prototype system B2TLA⁺ is successfully used to transform a temporal B model into a TLA⁺ module.

Conclusion

The paper successfully defines an approach for the specification and verification of safety and liveness properties for the development of reactive systems using the Event-B method, the language TLA⁺ and the predicate diagrams with their associated tools. The approach is illustrated on a case study of a parcel sorting system.     

Verifying concurrent probabilistic systems using probabilistic-epistemic logic specifications

In this paper, we address the problem of verifying probabilistic and epistemic properties in concurrent probabilistic systems expressed in PCTLK. PCTLK is an extension of the Probabilistic Computation Tree Logic (PCTL) augmented with Knowledge (K). In fact, PCTLK enjoys two epistemic modalities K_i for knowledge and \(Pr_{\triangledown b}K_{i}\) for probabilistic knowledge. The approach presented for verifying PCTLK specifications in such concurrent systems is based on a transformation technique. More precisely, we convert PCTLK model checking into the problem of model checking Probabilistic Branching Time Logic (PBTL), which enjoys path quantifiers in the range of adversaries. We then prove that model checking a formula of PCTLK in concurrent probabilistic programs is PSPACE-complete. Furthermore, we represent models associated with PCTLK logic symbolically with Multi-Terminal Binary Decision Diagrams (MTBDDs), which are supported by the probabilistic model checker PRISM. Finally, an application, namely the NetBill online shopping payment protocol, and an example about synchronization illustrated through the dining philosophers problem are implemented with the MTBDD engine of this model checker to verify probabilistic epistemic properties and evaluate the practical complexity of this verification.     

Security invariants in discrete transition systems

The Shadow semantics is a qualitative model for noninterference security for sequential programs. In this paper, we first extend the Shadow semantics to Event-B, to reason about discrete transition systems with noninterference security properties. In particular, we investigate how these security properties can be specified and proved as machine invariants. Next we highlight the role of security invariants during refinement and identify some common patterns in specifying them. Finally, we propose a practical extension to the supporting Rodin platform of Event-B, with the possibility of having some properties to be invariants-by-construction.     

基于Event-B 方法的多应用智能卡的建模与开发

Event-B是一种基于集合论和谓词逻辑的形式化系统语言,能够采用精化策略为系统建立逐渐精化的模型。提出了如何将Event B应用到实际工业领域的方法,包括重写需求、建立抽象模型及逐层精化三个步骤。首先从环境、功能、性质三个主要方面重写需求,明确精化策略;然后利用形式化方法建立抽象模型并验证该模型;最后,在正确的抽象模型上按照精化策略添加需求、逐层精化,并对每层模型进行验证,基于满足需求的最后一层模型,可进一步利用工具完成代码自动生成。该方法学采用精化理论,以逐层递增的方式明确被开发系统的需求及性质,并进行形式化建模与验证,确保了模型的正确性。为了说明该方法学的可行性,以真正工业界的多应用智能卡为实例,基于Event-B方法及其工具平台Rodin给出了该方法在实际建模及验证过程中的应用。     

Verifying data refinements using a model checker

In this paper, we consider how refinements between state-based specifications (e.g., written in Z) can be checked by use of a model checker. Specifically, we are interested in the verification of downward and upward simulations which are the standard approach to verifying refinements in state-based notations. We show how downward and upward simulations can be checked using existing temporal logic model checkers.In particular, we show how the branching time temporal logic CTL can be used to encode the standard simulation conditions. We do this for both a blocking, or guarded, interpretation of operations (often used when specifying reactive systems) as well as the more common non-blocking interpretation of operations used in many state-based specification languages (for modelling sequential systems). The approach is general enough to use with any state-based specification language, and we illustrate how refinements between Z specifications can be checked using the SAL CTL model checker using a small example.     

Verifying Contextual Refinement with Ownership Transfer

Contextual refinement is a compositional approach to compositional verification of concurrent objects.There has been much work designing program logics to prove the contextual refinement between the object implementation and its abstract specification.However,these program logics for contextual refinement verification cannot support objects with resource ownership transfer,which is a common pattern in many concurrent objects,such as the memory management module in OS kernels,which transfers the allocated memory block between the object and clients.In this paper,we propose a new approach to give abstract and implementation independent specifications to concurrent objects with ownership transfer.We also design a program logic to verify contextual refinement of concurrent objects w.r.t.their abstract specifications.We have successfully applied our logic to verifying an implementation of the memory management module,where the implementation is an appropriately simplified version of the original version from a real-world preemptive OS kernel.     

Relational concurrent refinement part III: traces,partial relations and automata

Data refinement in a state-based language such as Z is defined using a relational model in terms of the behaviour of abstract programs. Downward and upward simulation conditions form a sound and jointly complete methodology to verify relational data refinements, which can be checked on an event-by-event basis rather than per trace. In models of concurrency, refinement is often defined in terms of sets of observations, which can include the events a system is prepared to accept or refuse, or depend on explicit properties of states and transitions. By embedding such concurrent semantics into a relational framework, eventwise verification methods for such refinement relations can be derived. In this paper, we continue our program of deriving simulation conditions for process algebraic refinement by defining further embeddings into our relational model: traces, completed traces, failure traces and extension. We then extend our framework to include various notions of automata based refinement.     

Verifying a quantitative relaxation of linearizability via refinement

The recent years have seen increasingly widespread use of highly concurrent data structures in both multi-core and distributed computing environments, thereby escalating the priority for verifying their correctness. Quasi linearizability is a quantitative variation of the standard linearizability correctness condition to allow more implementation freedom for performance optimization. However, ensuring that the implementation satisfies the quantitative aspect of this new correctness condition is often an arduous task. In this paper, we propose the first automated method for formally verifying quasi linearizability of the implementation model of a concurrent data structure with respect to its sequential specification. The method is based on checking a relaxed version of the refinement relation between the implementation model and the specification model through explicit state model checking. Our method can directly handle concurrent systems where each thread or process makes infinitely many method calls. Furthermore, unlike many existing verification methods, it does not require the user to supply annotations of the linearization points. We have implemented the new method in the PAT verification framework. Our experimental evaluation shows that the method is effective in verifying the new quasi linearizability requirement and detecting violations.     

A state/event-based model-checking approach for the analysis of abstract system properties

We present the UMC framework for the formal analysis of concurrent systems specified by collections of UML state machines. The formal model of a system is given by a doubly labelled transition system, and the logic used to specify its properties is the state-based and event-based logic UCTL. UMC is an on-the-fly analysis framework which allows the user to interactively explore a UML model, to visualize abstract behavioural slices of it and to perform local model checking of UCTL formulae. An automotive scenario from the service-oriented computing (SOC) domain is used as case study to illustrate our approach.     

A semantic framework for the abstract model checking of tccp programs

The Timed Concurrent Constraint programming language (tccp) introduces time aspects into the Concurrent Constraint paradigm. This makes tccp especially appropriate for analyzing timing properties of concurrent systems by model checking. However, even if very compact state representations are obtained thanks to the use of constraints in tccp, large state spaces can still be generated, which may prevent model-checking tools from verifying tccp programs completely. Model checking tccp programs is a difficult task due to the subtleties of the underlying operational semantics, which combines constraints, concurrency, non-determinism and time. Currently, there is no practical model-checking tool that is applicable to tccp. In this work, we introduce an abstract methodology which is based on over- and under-approximating tccp models and which mitigates the state explosion problem that is common to traditional model-checking algorithms. We ascertain the conditions for the correctness of the abstract technique and show that this preliminary abstract semantics does not correctly simulate the suspension behavior, which is a key feature of tccp. Then, we present a refined abstract semantics which correctly models suspension. Finally, we complete our methodology by approximating the temporal properties that must be verified.     

Specification, Refinement and Verification of Concurrent Systems—An Integration of Object-Z and CSP

This paper presents a method of formally specifying, refining and verifying concurrent systems which uses the object-oriented state-based specification language Object-Z together with the process algebra CSP. Object-Z provides a convenient way of modelling complex data structures needed to define the component processes of such systems, and CSP enables the concise specification of process interactions. The basis of the integration is a semantics of Object-Z classes identical to that of CSP processes. This allows classes specified in Object-Z to be used directly within the CSP part of the specification.In addition to specification, we also discuss refinement and verification in this model. The common semantic basis enables a unified method of refinement to be used, based upon CSP refinement. To enable state-based techniques to be used for the Object-Z components of a specification we develop state-based refinement relations which are sound and complete with respect to CSP refinement. In addition, a verification method for static and dynamic properties is presented. The method allows us to verify properties of the CSP system specification in terms of its component Object-Z classes by using the laws of the CSP operators together with the logic for Object-Z.     

Unifying Concurrent and Relational Refinement

Refinement in a concurrent context, as typified by a process algebra, takes a number of different forms depending on what is considered observable, where observations record, for example, which events a system is prepared to accept or refuse. Examples of concurrent refinement relations include trace refinement, failures-divergences refinement and bisimulation.Refinement in a state-based language such as Z, on the other hand, is defined using a relational model in terms of input/output behaviour of abstract programs. These refinements are verified by using two simulation rules which help make the verification tractable.The purpose of this paper is to unify these two standpoints, and we do so by generalising the standard relational model to include additional observable aspects. The central result of the paper is then to develop simulation rules to verify relations such as failures-divergences refinement in a relational setting, and show how these might be applied in a specification language such as Z.     

Event-B patterns and their tool support

Event-B has given developers the opportunity to construct models of complex systems that are correct-by-construction. However, there is no systematic approach, especially in terms of reuse, which could help with the construction of these models. We introduce the notion of design patterns within the framework of Event-B to shorten this gap. Our approach preserves the correctness of the models, which is critical in formal methods and also reduces the proving effort. Within our approach, an Event-B design pattern is just another model devoted to the formalisation of a typical sub-problem. As a result, we can use patterns to construct a model which can subsequently be used as a pattern to construct a larger model. We also present the interaction between developers and the tool support within the associated RODIN Platform of Event-B. The approach has been applied successfully to some medium-size industrial case studies.     

Foundations for using linear temporal logic in Event-B refinement

In this paper we present a new way of reconciling Event-B refinement with linear temporal logic (LTL) properties. In particular, the results presented in this paper allow properties to be established for abstract system models, and identify conditions to ensure that the properties (suitably translated) continue to hold as those models are developed through refinement. There are several novel elements to this achievement: (1) we identify conditions that allow LTL properties to be mapped across refinement chains; (2) we provide translations of LTL predicates to reflect the introduction through refinement of new events and the renaming and splitting of existing events; (3) we do this for an extended version of LTL particularly suited to Event-B, including state predicates and enabledness of events, which can be model-checked at the abstract level. Our results are more general than any previous work in this area, covering liveness in the context of anticipated events, and relaxing constraints between adjacent refinement levels. The approach is illustrated with a case study. This enables designers to develop event based models and to consider their execution patterns so that liveness and fairness properties can be verified for Event-B systems.     

Formal verification of static software models in MDE: A systematic review

ContextModel-driven Engineering (MDE) promotes the utilization of models as primary artifacts in all software engineering activities. Therefore, mechanisms to ensure model correctness become crucial, specially when applying MDE to the development of software, where software is the result of a chain of (semi)automatic model transformations that refine initial abstract models to lower level ones from which the final code is eventually generated. Clearly, in this context, an error in the model/s is propagated to the code endangering the soundness of the resulting software. Formal verification of software models is a promising approach that advocates the employment of formal methods to achieve model correctness, and it has received a considerable amount of attention in the last few years.ObjectiveThe objective of this paper is to analyze the state of the art in the field of formal verification of models, restricting the analysis to those approaches applied over static software models complemented or not with constraints expressed in textual languages, typically the Object Constraint Language (OCL).MethodWe have conducted a Systematic Literature Review (SLR) of the published works in this field, describing their main characteristics.ResultsThe study is based on a set of 48 resources that have been grouped in 18 different approaches according to their affinity. For each of them we have analyzed, among other issues, the formalism used, the support given to OCL, the correctness properties addressed or the feedback yielded by the verification process.ConclusionsOne of the most important conclusions obtained is that current model verification approaches are strongly influenced by the support given to OCL. Another important finding is that in general, current verification tools present important flaws like the lack of integration into the model designer tool chain or the lack of efficiency when verifying large, real-life models.     

An event-based approach for formally verifying runtime adaptive real-time systems

Real-time and embedded systems are required to adapt their behavior and structure to runtime unpredicted changes in order to maintain their feasibility and usefulness. These systems are generally more difficult to specify and verify owning to their execution complexity. Hence, ensuring the high-level design and the early verification of system adaptation at runtime is very crucial. However, existing runtime model-based approaches for adaptive real-time and embedded systems suffer from shortcoming linked to efficiently and correctly managing the adaptive system behavior, especially that a formal verification is not allowed by modeling languages such as UML and MARTE profile. Moreover, reasoning about the correctness and the precision of high-level models is a complex task without the appropriate tool support. In this work, we propose an MDE-based framework for the specification and the verification of runtime adaptive real-time and embedded systems. Our approach stands for Event-B method to formally verify resources behavior and real-time constraints. In fact, thanks to MDE M2T transformations, our proposal translates runtime models into Event-B specifications to ensure the correctness of runtime adaptive system properties, temporal constrains and nonfunctional properties using Rodin platform. A flood prediction system case study is adopted for the validation of our proposal.

     

Core Hybrid Event-B III: Fundamentals of a reasoning framework

The Hybrid Event-B framework was introduced to add continuously varying behaviour to the discrete changes of state characteristic of the well established Event-B method. This is made necessary by the needs of verifying the hybrid and cyber-physical systems that are increasingly prevalent today. The semantic foundation of Hybrid Event-B rests on piecewise absolutely continuous functions of time. This enables unproblematic modelling of all classical physical phenomena, as well as the specification of conventional discrete changes of state, regardless of whether these arise in the physical arena or as abstractions of computational behaviour. In this paper, the large gap between arbitrary piecewise absolutely continuous functions, and what can be reasoned about mechanically/symbolically, is addressed. First, piecewise absolutely continuous real functions are restricted to piecewise complex analytic functions, real and without singularities on a semi-infinite portion of the real axis. This class has good properties with respect to symbolic manipulation and thus provides a good foundation for an approach to system verification that avoids dealing with the interleaved quantifiers of mathematical analysis, thus reducing the verification of the proof obligations of Hybrid Event-B to calculational checks. The individual proof obligations, whose discharge assures the correctness of a Hybrid Event-B machine, are examined, and results establishing sufficient conditions for their successful discharge via calculation are given. A small scale case study illustrates the verification process in this setting.