Search Results

Although Formal Methods have been used for decades in the development of industrial critical systems, there are still many products that do not use this technology. The use of Formal Methods in such a context is generally highly recommended, but ...

The increasing use of advanced smart contract structures in finance necessitates rigor and scalability in ensuring their correctness. Traditional auditing methods fall short in providing comprehensive security, but formal verification offers a ...

ProB provides a constraint solver for the B-method written in Prolog and can make use of different backends based on SAT and SMT solving. One such backend translates B and Event-B operators to SMT-LIB using the Z3 solver. This translation uses ...

Partial order reduction (POR) has considerable potential to reduce the state space during model checking by exploiting independence between transitions. This potential remains, however, largely unfulfilled for high-level formalisms such as B or ...

Automated model repair techniques enable machines to synthesise patches that ensure models meet given requirements. B-repair, which is an existing model repair approach, assists users in repairing erroneous models in the B formal method, but repairing ...

In software engineering, formal methods are often used to specify and verify design models of software products. Whether design models are consistent with required properties can significantly impact the quality of final software ...

• ISO/IEC 25010 can be used to evaluate the quality of state spaces.
• Twenty ...

B-method is a novel method developed by Beck et al. (SIAM J. Sci. Comput. 37(5), A2998–A3029, 2015), and has been shown theoretically to be very advantageous in time discretization of the second-order parabolic equations with blow-up solutions. In ...

In this article, we present a concrete realisation of the ETCS hybrid level 3 concept, whose practical viability was evaluated in a field demonstration in 2017. Hybrid level 3 introduces virtual subsections as sub-divisions of classical track ...

Relay-based Railway Interlocking Systems (RIS) are developed with the objective of controlling the movement of trains in a safe manner. However, these systems are generally specified by informal languages whose analyses are made by human ...

The B-method, which provides automated verification for the design of software systems, still requires users to manually repair faulty models. This paper proposes B-repair, an approach that supports automated repair of faulty models written in the ...

Constraint satisfaction problems can be expressed very elegantly in state-based formal methods such as B. But can such specifications be directly used for solving real-life problems? In other words, can a formal model be more than a design ...

In this article, we present our formalization of the ABZ landing gear case study in Event-B. The development was carried out using the Rodin platform and mainly used superposition refinement to structure the specification. To validate the model, we ...

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 ...

We present a translation of sequential ASMs to Event-B specifications. The translation also addresses the partial update problem, and allows a variable to be updated consistently in parallel. On the theoretical side, the translation highlights the ...

This paper presents a formal development of an Isabelle/HOL theory for the behavioral aspects of artifacts produced in the design of software components with the B method. We first provide a formalization of semantic objects such as labelled transition ...

We argue that B is a good language to conveniently express a wide range of constraint satisfaction problems. We also show that some problems can be solved quite effectively by the ProB tool. We illustrate our claim on several examples, such as the jobs ...

In this paper we describe the successful application of the ProB tool for data validation in several industrial applications. The initial case study centred on the San Juan metro system installed by Siemens. The control software was developed and ...

This paper proposes an approach connecting an automated control system, developed using formal methods, with an emulation of an environment where it is intended to operate. The motivation is to improve formal methods teaching by providing virtual ...

ProB is a model checker for high-level formalisms such as B, Event-B, CSP and Z. ProB uses a mixed depth-first/breadth-first search strategy, and in previous work we have argued that this can perform better in practice than pure depth-first or breadth-...

PROB is an animation and model checking tool, which supports integrated event- and state-based specifications combining B and CSP. We present an initial strategy for implementing the combined specification model as a concurrent Java program. Our Java ...