ABSTRACT. Many safety-critical system also contain requirements involving user interactions. Validating such requirements is typically done by techniques such as animation, trace replay, and LTL model checking. Interaction via animation and trace replay raise the problem that user and system/environment events are not separated. Formulating LTL properties requires considerable expertise. This work presents a new technique, called interactive simulation. The technique links domain-specific visualization of formal models with timed probabilistic simulation to create more realistic prototypes. In particular, domain experts and users can interact with formal models where upon system’s/environment’s reactions are simulated. For inspection of user interaction and system reaction, we also generate state diagrams from domain-specific components. Finally, we demonstrate and evaluate interactive simulation on the ABZ automotive case study

ABSTRACT. Crucible is a suite of tools supporting the use of Alloy as a functional specification language for high-integrity software systems. It incorporates a test generator, animator and range of supporting tools. Test generation is achieved by producing test conditions from the input Alloy model through equivalence partition and boundary value analysis, and then using the Alloy Analyzer to produce solutions. The solutions can optionally be converted into executable tests targeting a range of implementation languages. The advanced animator allows scenarios to be defined by users and run to help stakeholders validate the Alloy model. The animator uses an incremental solving approach whereby each animation step is solved separately and appropriate data carried forward between steps to give a scalable means to generate long scenarios. Additional GUIs and visualization facilities are included to make the tools accessible to as many stakeholders as possible. In this paper, we provide an overview of the technology behind the tools, initial results obtained with industrial case studies, and highlight some of the most interesting features and challenges.

ABSTRACT. Modelling hybrid systems using Event-B is challenging and users typically are unsure about whether their Event-B models are over/under-specified. In this short paper, we present a work-in-progress specification language called Cyclone to tackle this challenge. We demonstrate how one can use Cyclone to check an Event-B hybrid model using a car controller as an example. Our demonstration shows that Cyclone has a great potential to be used to verify Event-B hybrid models.

ABSTRACT. Reasoning and validating complex formal models is an intricate process. One of the primary reasons for this intricacy is the noise coming from interactions among different properties introduced at multiple levels of refinements. However, if we remove the noise, the consistency of the model needs to be reasserted along with the assumption that the findings from the simplified noiseless model still hold in the original complex model. To this end, this paper presents the AVoiR (Abstraction - Validation Obligation-Refinement) framework to help validate properties in complex formal models. The triptych AVoiR framework operates in the following fashion: 1) Using the abstraction technique, we first simplify a complex model by abstracting away the noise, i.e., removing the information unrelated to properties under analysis. This is done in a strictly controlled manner, preserving the consistency of the model. 2) Then, using the Validation Obligations (VOs) technique, we formalize what we want to observe to validate the desired property. 3) Finally, using the technique of VO refinement, we re-execute the VOs of the abstract model in the original model. Through this process, we focus on validating a property in a simplified model and then systematically transfer the findings to the original complex model. We use a case study from the aviation domain to show the proposed framework's efficacy.

ABSTRACT. This short paper summarizes an article published in the Journal of Automated Reasoning [6]. It presents Pardinus, an extension of the popular Kodkod [11] relational model finder with linear temporal logic (including past operators) to simplify the analysis of dynamic systems. Pardinus includes a SAT-based bounded-model checking engine and an SMV-based complete model checking engine, both allowing iteration through the different instances (or counter-examples) of a specification. It also supports a decomposed parallel analysis strategy that improves the efficiency of both analysis engines on commodity multi-core machines.

ABSTRACT. As the formal verification of safety-critical software systems often requires the integration of multiple tools and techniques, we propose a three-phase methodology incorporating two complementary workflows to ensure that the system in question fulfills its requirements. We use the Formal Requirements Elicitation Tool (FRET) to structure the requirements so that they can be translated to other formalisms. These translations are then either incorporated directly into an existing model in Simulink, or used to construct a new formal model of the system. Our current use case is a model of a controller for a civilian aircraft engine.

ABSTRACT. The modeling language of classical B is used to write specifications of various systems.Tools like ProB are able to use modelchecking techniques toverify invariants of these specifications such as safety-properties.However, classical B historically supports only discretemodels and has additionally no notion of floating-point numbers and real numbers. Currently challenging scenarios and issues which any suitable solution must address are explored. An approach is proposed such that ProB may offer such a solution in the future.

ABSTRACT. N/A

ABSTRACT. TLAPS, the TLA+ proof system, is a proof assistant for the development and mechanical verification of TLA+ proofs. TLAPS provides an interactive proof environment that relies on users guiding the proof effort, it integrates automatic proof search backends to discharge proof obligations, such as satisfiability modulo theories (SMT) and tableau provers. Currently, TLAPS supports three main backend provers, which are Isabelle/TLA+ (an encoding of TLA+ semantics in Isabelle), the tableau method prover Zenon, and a backend for SMT solvers. Nevertheless, to maintain the trustworthiness of proof generated by an SMT- solver, we want to reconstruct the resulting SMT proofs back into TLAPS. Currently, TLAPS does not verify the generated proof found by the SMT solver backend and only considers if the SMT-solver founds proof. Therefore, adding a reconstruction process of generated proofs in TLAPS will improve our trust in TLA+ proof. In order to achieve this aim, we present in the next sections an ongoing proposal for reconstructing proof obligations of TLAPS generated by the SMT solver veriT within the logical framework Lambdapi.