SafeCap is a modern toolkit for modelling, simulation and formal verification of railway networks. This paper discusses the use of SafeCap for formal analysis and automated scalable safety verification of solid state interlocking (SSI) programs – a technology at the heart of many railway signalling solutions around the world. The main driving force behind SafeCap development was to make it easy for signalling engineers to use the technology and thus to ensure its smooth industrial deployment. The unique qualities and the novelty of SafeCap are in making the use of formal notations and proofs fully transparent for the engineers. In this paper we explain the formal foundations of the proposed method, its tool support, and its successful application by railway companies in developing industrial signalling projects.

Industry applications of formal verification to signaling control tables require formulation of a large number of mathematical conjectures expressing verification rules. It is paramount to establish the validity and completeness of these conjectures. This article discusses a mutation-based validation technique that guides domain experts in the construction of such verification rules. Furthermore, we use genetic programming to quickly generate millions of well-formed data mutations of control tables and to synthesize mutation programs. The technique is illustrated by a synthetic running example and a discussion of our experience in using it in the industrial setting.

Abstract Dependability is a property of a computer system to deliver services that can be justifiably trusted. Formal modelling and verification techniques are widely used for development of dependable computer-based systems to gain confidence in the correctness of system design. Such techniques include Event-B—a state-based formalism that enables development of systems correct-by-construction. While Event-B offers a scalable approach to ensuring functional correctness of a system, it leaves aside modelling of non-functional critical properties, e.g., reliability and responsiveness, that are essential for ensuring dependability of critical systems. Both reliability, i.e., the probability of the system to function correctly over a given period of time, and responsiveness, i.e., the probability of the system to complete execution of a requested service within a given time bound, are defined as quantitative stochastic measures. In this paper, we propose an extension of the Event-B semantics to enable stochastic reasoning about dependability-related non-functional properties of cyclic systems. We define the requirements that a cyclic system should satisfy and introduce the notions of reliability and responsiveness refinement. Such an extension integrates reasoning about functional correctness and stochastic modelling of non-functional characteristics into the formal system development. It allows the designer to ensure that a developed system does not only correctly implement its functional requirements but also satisfies given non-functional quantitative constraints.

International audience

Wireless sensor–actor networks are a recent development of wireless networks where both ordinary sensor nodes and more sophisticated and powerful nodes, called actors, are present. In this paper we introduce several, increasingly more detailed, formal models for this type of wireless networks. These models formalise a recently introduced algorithm for recovering actor–actor coordination links via the existing sensor infrastructure. We prove via refinement that this recovery is correct and that it terminates in a finite number of steps. In addition, we propose a generalisation of our formal development strategy, which can be reused in the context of a wider class of networks. We elaborate our models within the Event-B formalism, while our proofs are carried out using the RODIN platform — an integrated development framework for Event-B.

Modes are widely used to structure the behaviour of control systems. For many such systems, derivation and verification of a mode logic is challenging due to a large number of modes and complex mode transitions. In this paper we propose an approach to deriving, formalising and verifying consistency of a mode logic for fault tolerant control systems. We demonstrate how to use Failure Modes and Effects Analysis (FMEA) to systematically derive the fault tolerance part of the mode logic. To tackle the problem of mode consistency, we propose a formalisation of the mode logic and mode consistency conditions for layered systems with reconfigurable components. We use our formalisation to develop and verify a mode-rich system by refinement in Event-B.

Developing fault tolerant ambient systems requires many challenging factors to be considered due to the nature of such systems, which tend to contain a lot of mobile elements that change their behavior depending on the surrounding environment, as well as the possibility of their disconnection and reconnection. It is therefore necessary to construct the critical parts of fault tolerant ambient systems in a rigorous manner. This can be achieved by deploying formal approach at the design stage, coupled with sound framework and support at the implementation stage. In this paper, we briefly describe a middleware that we developed to provide system structuring through the concepts of roles, agents, locations and scopes, making it easier for the developers to achieve fault tolerance. We then outline our experience in developing an ambient lecture system using the combination of formal approach and our middleware

Currently UML2 is widely used for modelling software-intensive systems. Model driven development of complex software typically starts from abstract, high-level UML2 models which specify the system from several different viewpoints. Abstract models are further refined into more detailed design models in successive development stages. While specifying various aspects and abstraction levels of such systems, we create a set of different models, which should be inter- and intra-consistent. In this paper we propose an approach to ensuring consistency in Lyra – a rigorous, service-oriented and model-based method for developing industrial telecommunication systems and communication protocols. We derive informal requirements to ensuring intra- and inter-consistency and then formalize them in the B Method. The formalization in B allows us to structure complex informal requirements and formally ensure intra- and inter-consistency of models created at various stages of the Lyra development.