Search

We report on case studies in which some variants of Anderson Protocol, an array-based queuing mutual exclusion protocol, have been analyzed with Maude, a rewriting logic-based computer language equipped with many facilities, such as model checking ones, and SMGA, a state machine graphical animation tool. We demonstrate that graphical state images help human users grasp some characteristics owned by each state. We also demonstrate that the divide & conquer approach to liveness model checking under fairness makes it feasible to conduct a liveness model checking under fairness that cannot be otherwise completed in a reasonable amount of time.

In this paper it is presented a software development model based on transformations that allows to derive, in an automatic way, classes in object-oriented programming languages (Ada 95, C++, Eiffel and Java) starting from formal specifications. The set of transformations that conforms the software development model are a systematic steps, which starts from the algebraic specification of a type. This algebraic specification describes the abstract behavior of a type (type of interest) by means of other type, previously specified and implemented (representation type). In a progressive way, the transformations steps allow get a program (class) nearby to the initial specification (type of interest). These transformations obtain -in the first step- an intermediate specification (class specification) that it describes the operations of the type of interest by means of pre and post-conditions. Then, the intermediate specification is used to obtain imperative code in language-independent notation (pseudo-class); and finally the pseudo-class is transformed to any object- oriented programming language for which it has been defined transformations.

Specifications define systems. The definition of a system can be stated casually or formally. A formal specification is a mathematically precise definition of software functionality. Informal specifications are less precise definitions of software functionality. The benefits of formal specifications are clear. Arguments against the use of formal specifications have been refuted. Several formal specification techniques are available for specifying imperative programs, e.g., Z, VDM, and SPECS. Most specification techniques for distributed/concurrent systems concentrate on low level issues, e.g., deadlock and synchronization. Structured Analysis (SA) specifications are a popular informal specification technique, but they lack a rigorous mathematical semantics. SA specifications are based on a graphical syntax with little underlying formal structure. In this thesis, we identify and formalize those underlying structures that are represented informally, provide a formal definition of a SA specification, develop formal interpretations for those components of SA specifications that are subject to varying interpretation, and define an operational semantics for animating SA specifications. The resulting formalized SA specifications are mathematically precise and can be used to specify distributed/concurrent systems.

Formal model-based specifications provide precise descriptions of the behavior of software components. These formal specifications are written using pre- and post-condition assertions. They can serve as a basis for formally verifying the correctness of an implementation. But a formal specification is really only useful when it captures the desired functionality. How can the specifier be confident that the specification is correct? The Abstract Test Tool supports the direct execution of C++ class specifications through the incremental development and automated generation of abstract test cases and the display of abstract results—both in terms of the abstract model used in the specification. The Class Validation System builds upon the Abstract Test Tool to support the automated and extensive testing of C++ class implementations. The Class Validation System provides a potentially one-to-many mapping from abstract test cases to implementation test cases. The results of executing the implementation are automatically compared to the results of executing the specification by mapping the implementation results to the abstract model. Thus, the Class Validation System supports fully automated implementation testing.

Executable specifications can serve as prototypes of the specified system and as oracles for automated testing of implementations, and so are more useful than non-executable specifications. Executable specifications can also be debugged in much the same way as programs, allowing errors to be detected and corrected at the specification level rather than in later stages of software development. However, existing executable specification languages often force the specifier to work at a low level of abstraction, which negates many of the advantages of non-executable specifications. This dissertation shows how to execute specifications written at a level of abstraction comparable to that found in specifications written in non-executable specification languages. The key innovation is an algorithm for evaluating and satisfying first order predicate logic assertions written over abstract model types. This is important because many specification languages use such assertions. Some of the features of this algorithm were inspired by techniques from constraint logic programming.

So far, valuable researches have been conducted on mapping object-oriented specification notations, such as Object-Z, to different object-oriented programming languages, such as C++. However, the results of selecting JVM-based programming languages for mapping have not covered most of basic Object-Z structures. In this paper, the Groovy language, as a dynamic JVM-based language, is selected to overcome some of the existing limitations. As the main contribution, the rules required for mapping Object-Z specifications to executable Groovy code are introduced. The proposed rules cover notions such as multiple inheritance, inverse specification of functions, functions defined on generic definitions, and free type constructors. These notions have not been covered in previous methods for formal program development from object-oriented specifications, regardless of the selected formal specification language and target programming language. In addition, in this paper, the parallel composition construct is mapped to a parallel, executable code to improve the faithfulness of the final code to the initial specification. We also introduce a mapping rule for the class union construct, which has not yet been provided for any JVM-based language. Unlike previous works, instead of presenting the mapping rules in terms of natural languages, we present them in terms of some formal mapping rules.

Declarative behavioural modelling is a powerful modelling paradigm that enables users to model system functionality abstractly and concisely. We compare two well-used formal declarative modelling languages, B and TLA+, with a new modelling language called Dash. Dash is an extension of Alloy with explicit syntactic constructs for modelling transition systems, and it includes control state hierarchy and events. Particular topics that we cover in our comparison are: differences in the datatypes and type systems; how the transitions/operations can be described; how the transition relation is a combination of the transitions; and the default choice each language makes regarding permitted variable changes in a transition. Our goal is to discuss the interesting differentiating characteristics of each language to aid users in determining which language is the most suitable for their system.

We describe a method and tools for deriving specification models from requirements, and for validating that the final software product satisfies the requirements. ETF (Eiffel Testing Framework) is a tool for generating code from an abstract grammar specification of user interface actions derived from the requirements document. Mathmodels extends the classical Eiffel contracting notation with the use of mathematical models (based on sets, sequences, relations, functions, bags). The Mathmodels library has immutable queries (for specifications) as well as relatively efficient mutable commands (for describing executable abstract state machines). Models are developed and validated using the industrial strength Eiffel IDE, and the use of these tools thus scale up to the development of large systems in a way that supports the derivation of specification models from requirements, and seamlessness between models and code.

Procedure specifications are useful in many software development tasks. As one example, in automatic test case generation they can guide testing, act as test oracles able to reveal bugs, and identify illegal inputs. Whereas formal specifications are seldom available in practice, it is standard practice for developers to document their code with semi-structured comments. These comments express the procedure specification with a mix of predefined tags and natural language. This paper presents Jdoctor, an approach that combines pattern, lexical, and semantic matching to translate Javadoc comments into executable procedure specifications written as Java expressions. In an empirical evaluation, Jdoctor achieved precision of 92% and recall of 83% in translating Javadoc into procedure specifications. We also supplied the Jdoctor-derived specifications to an automated test case generation tool, Randoop. The specifications enabled Randoop to generate test cases of higher quality.

International audience; Template-Coq is a plugin for Coq, originally implemented by Malecha, which provides a reifier for Coq terms and global declarations , as represented in the Coq kernel, as well as a denotation command. Initially, it was developed for the purpose of writing functions on Coq's AST in Gallina. Recently, it was used in the CertiCoq certified compiler project, as its front-end language, to derive parametricity properties, and to extract Coq terms to a CBV λ-calculus. However, the syntax lacked semantics, be it typing semantics or operational semantics, which should reflect, as formal specifications in Coq, the semantics of Coq's type theory itself. The tool was also rather bare bones, providing only rudimentary quoting and unquoting commands. We generalize it to handle the entire Calculus of Inductive Constructions (CIC), as implemented by Coq, including the kernel's declaration structures for definitions and inductives, and implement a monad for general manipulation of Coq's logical environment. We demonstrate how this setup allows Coq users to define many kinds of general purpose plugins, whose correctness can be readily proved in the system itself, and that can be run efficiently after extraction. We give a few examples of implemented plugins, including a parametricity translation. We also advocate the use of Template-Coq as a foundation for higher-level tools.

Unified modeling language (UML) is a standardized modeling language enabling to specify, construct and document artifacts of a software system based on graphical notations. However, UML lacks a firm semantics which reduces the quality of system models produced and leads to difficulties in automatic analysis and verification. In this paper, we propose an automatic translation from UML 2.0 Interaction Overview Diagrams (IOD) into Maude rewriting logic Language. Maude is used as a formal notation for specifying models and their firm semantics make models analysis and simulation easier. The approach is based on Graph Transformation and the Meta-Modeling tool AToM3 is used. The approach is illustrated through an example.

With the recent discoveries of widespread vulnerabilities, the use of formal methods in the design of system is more and more important, in particular in the context of Cloud computing which can be used for high performance computing applications [1]. Formal methods range from more lightweight method such as the Alloy [2] formal specification language and analyzer to more heavyweight formal methods based on proof assistants such as Isabelle/HOL or Coq [3].

UML is a semi-formal notation largely adopted in the industry as the standard language for software design and analysis. Its imprecise semantics prevents any verification task. However, a formal semantics can be given to UML diagrams, for instance, through their transformation to models with a formal semantics, such as Colored Petri Nets (CPN). Colored Petri nets are an efficient language for UML state machine formalization and analysis. In order to assist the UML modeler in understanding the report generated by the Petri net tool, we propose a method to construct UML diagrams from the returned report. A case study is given to illustrate the proposed approach.

International audience; This paper is about the extension of the SysML/KAOS requirements engineering method with domain models expressed as ontologies. More precisely, it concerns the translation of these ontologies into B System for system construction. The contributions of this paper are twofold. The first one is a formal semantics for the ontology modeling language. The second one is the formal definition of translation rules between ontologies and B system specifications in order to provide the structural part of the formal specification. These translation rules are modeled in Event-B. Their consistency and completeness are proved using Rodin. We show that they are structure preserving (two related elements within the source model remain related within the target model), by proving various isomorphisms between the ontology and the B System specification

International audience; This paper presents a specification of the hybrid ERTMS/ ETCS level 3 standard in the framework of the case study proposed for the 6th edition of the ABZ conference. The specification is based on the method and tools, developed in the ANR FORMOSE project, for the modeling and formal verification of critical and complex system requirements. The requirements are specified with SysML/KAOS goal diagrams and are automatically translated into B System specifications, in order to obtain the architecture of the formal specification. Domain properties are specified by ontologies with the SysML/KAOS domain modeling language, based on OWL and PLIB. Their automatic translation completes the structural part of the formal specification. The only part of the specification, which must be manually completed, is the body of events. The construction is incremental, based on the refinement mechanisms existing within the involved methods. The formal specification of the case study is composed of seven refinement levels and all the proofs have been discharged with the Rodin prover

In this paper, we provide a toolchain that facilitates the integration of formal verification techniques into model-based design. Applying verification tools to industrially relevant models requires three main ingredients: a formal model, a formal verification method, and a set of formal specifications. Our focus is on hybrid automata as the model and on reachability analysis as the method. Much progress has been made towards developing efficient and scalable reachability algorithms tailored to hybrid automata. However, it is not easy to encode rich formal specifications such that they can be interpreted by existing tools for reachability. Herein, we consider specifications expressed in pattern templates which are predefined properties with placeholders for state predicates. Pattern templates are close to the natural language and can be easily understood by both expert and non-expert users. We provide (i) formal definitions for selected patterns in the formalism of hybrid automata and (ii) monitors which encode the properties as the reachability of an error state. By composing these monitors with the formal model under study, the property can be checked by off-the-shelf fully automated verification tools. We illustrate the workflow on an electro-mechanical brake use case.

Operators are special characters within the Java language to manipulate primitive data type. Java operators can be classified as unary, binary and ternary. The design of Java operator sometimes becomes confusing when it comes to testing tools as they had the same function with different label in every testing tool. Therefore, in order to map the knowledge of operators correctly, this research has proposed ontology that is dedicated to mutation testing as a means to define the formal specification of concepts and documentation of knowledge of Java operators. Existing papers on ontology did not specify further on entities and properties of operators. Some papers only focus on mutation testing but not the operators. Thus, this paper will present the ontology clearly with the aim to ease end user to identify and understand every classes, properties and relations in Java operators.

In specification-based test generation, sometimes having a formal specification is not sufficient, since the specification may be in a different formalism from that required by the generation approach being used. In this paper, we deal with this problem specifically in the context in which, while having a formal specification in the form of an operational invariant written in a sequential pro- gramming language, one needs, for test generation, a declarative invariant in a logical formalism. We propose a genetic algorithm that given a catalog of common properties of invariants, such as acyclicity, sortedness and balance, attempts to evolve a conjunction of these that most accurately approximates an original operational specification. We present some details of the algorithm, and an experimental evaluation based on a benchmark of data structures, for which we evolve declarative logical invariants from operational ones.

International audience; This paper presents ongoing work to add a modular reset construct to a verified Lustre compiler. We present a novel formal specification for the construct and sketch our plans to integrate it into the compiler and its correctness proof.

International audience; The Cypher property graph query language is an evolving language, originally designed and implemented as part of the Neo4j graph database, and it is currently used by several commercial database products and researchers. We describe Cypher 9, which is the first version of the language governed by the openCypher Implementers Group. We first introduce the language by example, and describe its uses in industry. We then provide a formal semantic definition of the core read-query features of Cypher, including its variant of the property graph data model, and its " ASCII Art " graph pattern matching mechanism for expressing subgraphs of interest to an application. We compare the features of Cypher to other property graph query languages, and describe extensions, at an advanced stage of development, which will form part of Cypher 10, turning the language into a compositional language which supports graph projections and multiple named graphs.

This paper presents a software development process for safety-critical software components of cyber-physical systems. The process is called MINERVA, which stands for Mirrored Implementation Numerically Evaluated against Rigorously Verified Algorithms. The process relies on formal methods for rigorously validating code against its requirements. The software development process uses: (1) a formal specification language for describing the algorithms and their functional requirements, (2) an interactive theorem prover for formally verifying the correctness of the algorithms, (3) test cases that stress the code, and (4) numerical evaluation on these test cases of both the algorithm specifications and their implementations in code. The MINERVA process is illustrated in this paper with an application to geo-containment algorithms for unmanned aircraft systems. These algorithms ensure that the position of an aircraft never leaves a predetermined polygon region and provide recovery maneuvers when the region is inadvertently exited.

Despite the popularity and growing importance of OpenMP, a formal characterization of its concurrency is lacking. In this paper, we provide such a characterization through an operational semantics. Semantic descriptions of languages are written to serve specific end goals, and hence are abstractions of fully detailed implementations. We have developed our semantics to help with the construction of a novel OpenMP data race checker called Sword that collects execution traces efficiently, and subjects the traces to offline analysis: the semantics are used in the latter phase. Key contributions of this paper are: (1) defining OpenMP's concurrency rigorously through a precise set of rules, (2) helping systematically design Sword's offline analysis phase by ensuring that the OpenMP events mentioned in our semantics are exactly those that can also be collected through OMPT, a standard event collection mechanism for OpenMP, and (3) characterizing the benefits of this design. We conclude with the message that developing formal semantics for concurrent languages must not be viewed as an esoteric diversion, but as standard practice, as such semantics can help clearly define the language, help rigorously analyze proposed future extensions to it, and also help reveal lurking pitfalls, especially in this era where multiple concurrency formalisms are often used together.

International audience; We present TESTOR, a tool for on-the-fly conformance test case generation, guided by test purposes. Concretely, given a formal specification of a system and a test purpose, TESTOR automatically generates test cases, which assess using black box testing techniques the conformance to the specification of a system under test. In this context, a test purpose describes the goal states to be reached by the test and enables one to indicate parts of the specification that should be ignored during the testing process. Compared to the existing tool TGV, TESTOR has a more modular architecture, based on generic graph transformation components , is capable of extracting a test case completely on the fly, and enables a more flexible expression of test purposes, taking advantage of the multiway rendezvous. TESTOR has been implemented on top of the CADP verification toolbox, evaluated on three published case-studies and more than 10000 examples taken from the non-regression test suites of CADP.

International audience; Languages for loop transformations have been leveraged for different type of tools and frameworks in different application domains, yet they lack formal semantics. As a step towards formal specification, this works intends to clarify the underlying concepts of such languages using a denotational approach.

Testing grammars has one big difference from testing software: natural language has no formal specification, so ultimately we must involve a human oracle. However, we can automate many useful subtasks: detect ambiguous constructions and contradictory grammar rules, as well as generate minimal and representative set of examples that cover all the constructions. Think of the whole grammar as a haystack, and we suspect there are a few needles–we cannot promise automatic needle-removal, but instead we help the human oracle to narrow down the search.

The manual translation of informally defined requirements into statecharts, from which source code can be generated automatically, can be an error-prone, laborintensive process. Design errors sometimes propagate into final implementation code, only to be discovered during testing and verification. However, the requirements that the software needs to satisfy can be formally defined via temporal logics. In this paper, an approach to automatically synthesize flight-software hybrid-controllers for dynamic systems from formal specifications is given. First, specifications for a specific control functionality are defined by a set of linear temporal logic formulas. These, together with a model of the dynamical system, are then used as inputs to the Caltech-developed temporal logic planning toolbox (TuLiP), which searches for a control design. This results in a controller that is hybrid as it combines a finite state controller together with low-level continuous control actions. We map the resulting controller design to UML statecharts, which can be given as input to the Statechart Autocoder (SCA) developed by the Jet Propulsion Laboratory. SCA maps statechart controller designs to software implementation C code suitable for flight applications. By construction, the resulting code will meet the original formal design specifications, thus eliminating latent design errors. This paper describes the new 2nd generation interface developed to specify and convert the TuLiP-produced design to more optimized (e.g., reduced number of states and transitions) input UML (as XML file) for the JPL Statechart Autocoder. By applying intermediate optimization procedures, in which indistinguishable states are merged and transitions are grouped, the size of the statechart and the resulting code is reduced substantially. This is demonstrated by revisiting our 2016 speed-controller example showing reduction by more than 75% of the states synthesized in the original example.

Instruction selection is the part of a compiler that transforms intermediate representation (IR) code into machine code. Instruction selectors build on a library of hundreds if not thousands of rules. Creating and maintaining these rules is a tedious and error-prone manual process. In this paper, we present a fully automatic approach to create provably correct rule libraries from formal specifications of the instruction set architecture and the compiler IR. We use a hybrid approach that combines enumerative techniques with template-based counterexample-guided inductive synthesis (CEGIS). Thereby, we overcome several shortcomings of existing approaches, which were not able to handle complex instructions in a reasonable amount of time. In particular, we efficiently model memory operations. Our tool synthesized a large part of the integer arithmetic rules for the x86 architecture within a few days where existing techniques could not deliver a substantial rule library within weeks. Using the rule library, we generate a prototype instruction selector that produces code on par with a manually-tuned instruction selector. Furthermore, using 63012 test cases generated from the rule library, we identified 29498 rules that both Clang and GCC miss.

We present system VRS (Verification of Requirements Specifications) designed for develop- ment of formal specification and verification. This system has been developed by VRS Kiev group during last 10 years to support requirements capturing in Motorola and then Uniquesoft projects. As its input language VRS uses parameterized MSCs (Message Sequence Charts) with pre- and postconditions interpreted on the states of an environment with inserted agents. Such small MSC we call : Basic Protocols. Semantically basic protocol can be considered as a statement 8x(� ! �) of some kind of dynamic logic (2). In this statement x is a (typed) list of parameters, � andare precondition and postcondition, correspondingly, and u is a process defined by the MSC diagram. There are three main methods of verification in VRS supported by appropriate tools. The system provides static requirement checking on the base of automatic theorem proving; symbolic and deductive model checking, and generation of traces for testing with different coverage criteria. Concrete trace generator (CTG) of VRS system provide checking the reachability of properties, detecting deadlocks, non-determinisms, safety violations, unreachable requirements, usage of uninitialized attributes and admitted range attribute overflow on a base of a concrete model of formal requirement specification in the form of basic protocols. The problems above are solved by means of generating traces reachable from the initial state of a model. The generated traces can also be used for test generation. Symbolic Trace Generator (STG) deals with the same iput data as for CTG. The difference is that an abstract model of a system specified by a set of basic protocols is considered instead of a concrete one. The state of a model has the form (u1...un) where is a formula over attributes which coincides with the attributed label of the environment state and u1...un are agents inserted into environment. The deductive system is used for checking the applicability of basic protocol and predicate transformer is used to obtain the next state. Static requirement checking (SRC) tools allow to solve verification problems without generating traces and exploring the state space. The deductive system is based on the prover for the first order predicate calculi with equality extended by some special provers and solvers. THe last ones support proving and solving linear numerical constraints for integers (Presburger algorithm) and for reals (Fourier-Motzkin algorithm), proving and solving formulas for enumer- ated and symbolic data types. There is a possibility to generate invariants then SRC technique can be improved by iterative steps in sense that if F is not safety then VRS can generate an invariant G, improve safety property to F&G, and check safety repeatedly. In the last years this approach has been successfully applied to the problems of the veri- fication of requirement specifications (1, 3) for about 30 distributed concurrent systems from different subject domains including Telecommunications, Telematics, distributed computing and others.

Architectural design patterns capture architectural design experience and provide abstract solutions to recurring architectural design problems. Their description is usually expressed informally and it is not verified whether the proposed specification indeed solves the original design problem. As a consequence, an architect cannot fully rely on the specification when implementing a pattern to solve a certain problem. To address this issue, we propose an approach for the specification and verification of architectural design patterns. Our approach is based on interactive theorem proving and leverages the hierarchical nature of patterns to foster reuse of verification results. The following paper presents FACTum, a methodology and corresponding specification techniques to support the formal specification of patterns. Moreover, it describes an algorithm to map a given FACTum specification to a corresponding Isabelle/HOL theory and shows its soundness. Finally, the paper demonstrates the approach by verifying versions of three widely used patterns: the singleton, the publisher-subscriber, and the blackboard pattern.

Domain Specific Modelling Languages provide the designers with appropriate languages for the task they must conduct. These dedicated languages play a key role in popular Model Driven Engineering (MDE) approaches. Their semantics are usually written in a semi-formal manner mixing natural language and mathematical notations. The mechanization of these semantics rely on formal specification languages. They are usually conducted in order to assess the correctness of verification and transformation tools for such languages. This contribution illustrates such a mechanization for the Clock Constraint Specification Language (CCSL). This language allows to model the timed concurrency concern in the MARTE UML profile and was designed to be easier to master than temporal logics for the system engineers. Its semantics has been defined in the usual semi-formal manner and implemented in the TimeSquare simulation tool. We discuss the interest of this mechanization and show how it allowed to prove properties about this language and ease the definition of a refinement relation for such models. This work relies on the Agda proof assistant and is presented accordingly.

The article analyzes the difficulties which Bachelor Degree in Informatics and Computer Sciences students encounter in the process of being trained in applying deductive methods of verification and synthesis of procedural programs. Education in this field is an important step towards moving from classical software engineering to formal software engineering. The training in deductive methods is done in the introductory courses in programming in some Bulgarian universities. It includes: Floyd’s method for proving partial and total correctness of flowchart programs; Hoare’s method of verification of programs; and Djikstra’s method of transforming predicates for verification and synthesis of Algol−like programs. The difficulties which occurred during the defining of the specification of the program, which is subjected to verification or synthesis; choosing a loop invariant and loop termination function; finding the weakest precondition; proving the formulated verifying conditions, are discussed in the paper. Means of overcoming these difficulties is proposed. Conclusions are drawn in order to improve the training in the field. Special attention is dedicated to motivating the use of specific tools for software analysis, such as interactive theorem proving system HOL, the software analyzers Frama−C and its WP plug−in, as well as the formal language ACSL, which allows formal specification of properties of C/C++ programs.

Advances in theorem proving have enabled the emergence of a variety of formal developments that, over the years, have resulted in large corpuses of formalizations. For example, the NASA PVS Library is a collection of 55 formal developments written in the Prototype Verification System (PVS) over a period of almost 30 years and containing more than 28000 proofs. Unfortunately, the simple accumulation of formal developments does not guarantee their reusability. In fact, in formal systems with very expressive specification languages, it is often the case that a particular conceptual object is defined in different ways. This paper presents a technique to establish sound connections between formal definitions. Such connections support the possibility of (partial) borrowing of proved results from one formal description into another, improving the reusability of formal developments. The technique is described using concepts from the field of universal algebra and algebraic specification. The technique is illustrated with concrete examples taken from formalizations available in the NASA PVS Library.

Among formal methods, the deductive verification approach allows establishing the strongest possible formal guarantees on critical software. The downside is the cost in terms of human effort required to design adequate formal specifications and to successfully discharge the required proof obligations. To popularize deductive verification in an industrial software development environment, it is essential to provide means to progressively transition from simple and automated approaches to deductive verification. The SPARK environment, for development of critical software written in Ada, goes towards this goal by providing automated tools for formally proving that some code fulfills the requirements expressed in Ada contracts. In a program verifier that makes use of automatic provers to discharge the proof obligations, a need for some additional user interaction with proof tasks shows up: either to help analyzing the reason of a proof failure or, ultimately, to discharge the verification conditions that are out-of-reach of state-of-the-art automatic provers. Adding interactive proof features in SPARK appears to be complicated by the fact that the proof toolchain makes use of the independent, intermediate verification tool Why3, which is generic enough to accept multiple front-ends for different input languages. This paper reports on our approach to extend Why3 with interactive proof features and also with a generic client-server infrastructure allowing integration of proof interaction into an external, front-end graphical user interface such as the one of SPARK., In Proceedings F-IDE 2018, arXiv:1811.09014

The EMV® (EMV® is a registered trademark or trademark of EMVCo, LLC in the US and other countries.) organisation specify payment protocols to facilitate worldwide interoperability of secure electronic payments. This paper is about the application and scalability of formal methods to a current and complex industry application. We describe the use of VDM to model EMV® \(2^{nd}\) Generation Kernel (A preliminary version of this paper was presented at the \(16^{th}\) Overture Workshop, Oxford July 2018, where papers became a Newcastle Technical Report.). VDM is useful for both formal specification, as well as simulation, test coverage, and proof obligation generation for functional correctness.

Software development is costly endeavors. In general, the cost can be reduced by checking whether the program meets the specification. Usually, software is composed of several modules so that by checking the correctness of each module, developers can find the causes of errors efficiently. Formal verification and specification-based testing are effective techniques to verify programs. Formal verification based on Hoare logic can establish the correctness of programs from the theoretical point of view. However, it is regarded as an impractical technique for realistic programs, due to some challenges, On the other hand, specification-based testing is able to detect errors, and it is easy to perform. Therefore, it is frequently used for realistic developments. However, in most cases, the testing cannot guarantee the correctness of programs. As we described above, both of these techniques cannot do satisfactory job alone. To solve this problem, a novel verification approach was suggested, which is called testing-based formal verification (TBFV). In this paper, we aim to automate application of Hoare logic to Java programs based on the previously proposed TBFV. At the same time, we try to reveal the feasibility of TBFV through developing a supporting tool for Java programs and conducting a case study. At the same time, to achieve an effective automatic verification, we add the function of automatic boundary testing in the result evaluation step in the supporting tool. As a result, our supporting tool has achieved a semi-formal automation of Hoare logic application, which can help reduce the cost of verification process.

This paper investigates rewriting logic as a suitable means to model the semantics of distributed and concurrent systems implemented using Monitoring Oriented Programming (MOP) frameworks. MOP tools close the gap between specification and implementation, allowing several formal specifications and concrete implementations to be combined into a single executing system. To address real-time monitoring of modern distributed applications, we recently proposed REAL-T, a reactive event-based distributed programming language with explicit support for distributions and time manipulation. REAL-T allows programmers to instrument distributed applications to monitor and enforce specific behavior. It also supports requirements of modern reactive applications (responsiveness, resiliency, elasticity and asynchronous communication). The REAL-T programming model is very flexible, making the semantic specifications very challenging., Este artículo investiga la reescritura de la lógica como un medio adecuado para modelar la semántica de sistemas distribuidos y concurrentes implementados utilizando marcos de Programación Orientada a Monitoreo (MOP). Las herramientas MOP cierran la brecha entre la especificación y la implementación, permitiendo que varias especificaciones formales e implementaciones concretas se combinen en un solo sistema de ejecución. Para abordar el monitoreo en tiempo real de aplicaciones distribuidas modernas, recientemente propusimos REAL-T, un lenguaje de programación distribuida basado en eventos reactivos con soporte explícito para distribuciones y manipulación de tiempo. REAL-T permite a los programadores instrumentar aplicaciones distribuidas para monitorear y hacer cumplir un comportamiento específico. También es compatible con los requisitos de las aplicaciones reactivas modernas (capacidad de respuesta, resiliencia, elasticidad y comunicación asincrónica). El modelo de programación REAL-T es muy flexible, lo que hace que las especificaciones semánticas sean un gran desafío.

Analysis tools like abstract interpreters, symbolic execution tools and testing tools usually require a proper context to give useful results when analyzing a particular function. Such a context initializes the function parameters and global variables to comply with function requirements. However it may be error-prone to write it by hand: the handwritten context might contain bugs or not match the intended specification. A more robust approach is to specify the context in a dedicated specification language, and hold the analysis tools to support it properly. This may mean to put significant development efforts for enhancing the tools, something that is often not feasible if ever possible.

In this paper, a formal specification approach of the Attribute-Based Access Control (ABAC) is proposed using the Event-B method. We apply an a-priori formal verification to build a correct model in a stepwise manner. Correctness of the specification model is insured during the construction steps. The model is composed of abstraction levels that are generated through refinement operations. A set of ABAC properties is defined in each level of refinement starting from the highest abstract level to the most concrete one. These properties are preserved by proofs with the behavior specification.

Applying deductive verification to formally prove that a program respects its formal specification is a very complex and time-consuming task due in particular to the lack of feedback in case of proof failures. Along with a non-compliance between the code and its specification (due to an error in at least one of them), possible reasons of a proof failure include a missing or too weak specification for a called function or a loop, and lack of time or simply incapacity of the prover to finish a particular proof. This work proposes a methodology where test generation helps to identify the reason of a proof failure and to exhibit a counterexample clearly illustrating the issue. We define the categories of proof failures, introduce two subcategories of contract weaknesses (single and global ones), and examine their properties. We describe how to transform a C program formally specified in an executable specification language into C code suitable for testing, and illustrate the benefits of the method on comprehensive examples. The method has been implemented in StaDy , a plugin of the software analysis platform Frama -C. Initial experiments show that detecting non-compliances and contract weaknesses allows to precisely diagnose most proof failures.

In this paper, we present AsmetaA – a graphical animator for Abstract State Machines integrated within the ASMETA framework. The execution of formal specifications through animation provides several advantages, e.g., it provides an immediate feedback about system behavior, it helps understand system evolution, and it increases the overall acceptability of formal methods.

We introduce a new framework for verifying electronic vote counting results that are based on the Single Transferable Vote scheme (STV). Our approach frames electronic vote counting as certified computation where each execution of the counting algorithm is accompanied by a certificate that witnesses the correctness of the output. These certificates are then checked for correctness independently of how they are produced. We advocate verification of the verifier rather than the software used to produce the result. We use the theorem prover HOL4 to formalise the STV vote counting scheme, and obtain a fully verified certificate checker. By connecting HOL4 to the verified CakeML compiler, we then extract an executable that is guaranteed to behave correctly with respect to the formal specification of the protocol down to machine level. We demonstrate that our verifier can check certificates of real-size elections efficiently. Our encoding is modular, so repeating the same process for another different STV scheme would require a minimal amount of additional work.

Runtime verification is the discipline of analyzing program executions using rigorous methods. The discipline covers such topics as specification-based monitoring, where single executions are checked against formal specifications; predictive runtime analysis, where properties about a system are predicted/inferred from single (good) executions; specification mining from execution traces; visualization of execution traces; and to be fully general: computation of any interesting information from execution traces. Finally, runtime verification also includes fault protection, where monitors actively protect a running system against errors. The paper is written as a response to the ‘Test of Time Award’ attributed to the authors for their 2001 paper [45]. The present paper provides a brief overview of what lead to that paper, what has happened since, and some perspectives on the future of the field.

© 2017 IEEE. Nowadays, computer science increasingly uses formal methods to enhance understanding of complex software systems and to reason about their behavior with respect to a formal specification. To let future generations of software developers and engineers profit from these exciting developments, however, it is necessary to adequately educate and train them in the basics of formal logic and formal language semantics. However, preciously few software tools do exist that substantially aid this educational process. Because the semantics is an integral part of a formal definition of a programming language, we have prepared a package of modules, that help us and to students to understand the most popular semantic method - structural operational semantics. The first module translates a program written in a programming language to abstract machine code, the second module makes reverse translation from code to program source text and the third one emulates stepwise execution of abstract machine code. Our package can be easily extended for other semantic methods.

Static verification based on such methods as Bounded Model Checking and Counterexample-Guided Abstraction Refinement aims at non-interactive formal proving of programs correctness against safety property specifications. To leverage existing tools for verification of a program one should prepare verification tasks first. In addition to a program fragment of a moderate size, each verification task has to contain a rather accurate model of its environment. To achieve high-quality results this model should be incrementally refined in accordance with checked safety properties. For verification of specific software, like Windows or Linux drivers, a few frameworks provide a convenient user interface and perform in an automated way generation of verification tasks, execution of static verification tools and preliminary processing of results. This paper presents a method for automated static verification of any program developed in the GNU C programming language and addresses the ongoing development of the Klever framework.

Formal methods are mathematically based languages, tools and techniques for the specification, development and verification of systems [12]. Although most effort is being spent on specifying systems and verifying their properties, a final goal of most formal methods is achieving correct code from formal specifications. In this direction we find two representative strategies: (i) one is based on proposing refinements until a certain concrete design is achieved and then an almost direct mapping from mathematical elements to the source code of some programming language is made [17]; and (ii) another is using some refinement calculus in which specification and programming constructs are available in a single language and code is achieved by removing the specification elements by applying specific refinement rules [9]. Both strategies depend on developers experience.

Memory coherence is the most fundamental re-quirement in a shared virtual memory system where there are concurrent as well as loosely coupled processes. These processes can demand a page for reading or writing. The memory is called coherent if the last update in a page remains constant for each process until the owner of that page does not change it. The ownership is transferred to a process interested to update that page. In [Kai LI, and Paul Hudak. Memory Coherence in Shared Virtual Memory Systems, 1986. Proc. of Fifth Annual ACM Symposium on Principles of Distributed Computing.], algorithms ensuring memory coherence are given. We formally specify these protocols and report the improvements through formal analysis. The protocols are specified in UPPAAL, i.e., a tool for modeling, validation and verification of real-time systems.

The specification of a programming language is a special case of the specification of software in general. This paper discusses the relation between semantics and implementation, or specification and program, using two very different languages for illustration. First, we consider small fragments of a specification of preliminary Ada, and show that what was considered a specification in VDM in 1980 now looks much like an implementation in a functional language. Also, we discuss how a formal specification may be valuable even though seen from a purely formal point of view it is flawed. Second, we consider the simple language of spreadsheet formulas and give a complete specification. We show that nondeterminism in the specification may reflect run-time nondeterminism, but also underspecification, that is, implementation-time design choices. Although specification nondeterminism may appear at different binding-times there is no conventional way to distinguish these. We also consider a cost semantics and find that the specification may need to contain some “artificial” nondeterminism for underspecification.

This paper presents the formal specification and verification of a Type-1 (T1) Fuzzy Logic Rule-Based Classifier (FLRBC) using the Prototype Verification System (PVS). A rule-based system models a system as a set of rules, which are either collected from subject matter experts or extracted from data. Unlike many machine learning techniques, rule-based systems provide an insight into the decision making process. In this paper, we focus on a T1 FLRBC. We present the formal definition and verification of the T1 FLRBC procedure using PVS. This helps mathematically verify that the design intent is maintained in its implementation. A highly expressive language such as PVS, which is based on a strongly-typed higher-order logic, allows one to formally describe and mathematically prove that there is no contradiction or false assumption in the procedure. We show this by (1) providing the formal definition of the T1 FLRBC in PVS and then (2) formally proving or deducing rudimentary properties of the T1 FLRBC from the formal specification.