Verifying Object-based Graph Grammars

The development of concurrent and reactive systems is gaining importance since they are well-suited to modern computing platforms, such as the Internet. However, the development of correct concurrent and reactive systems is a non-trivial task. Object-based graph grammar (OBGG) is a visual formal language suitable for the specification of this class of systems. In previous work, a translation from OBGG to PROMELA (the input language of the SPIN model checker) was defined, enabling the verification of OBGG models using SPIN. In this paper we extend this approach in two different ways: (1) the approach for property specification is improved, enabling to prove properties not only about possible OBGG derivations, but also about the internal state of involved objects; (2) an approach is defined to interpret PROMELA races as OBGG derivations, generating graphical counter-examples for properties that are not true for a given OBGG model. Another contribution of this paper is (3) the definition of a method for model checking partial systems (isolated objects or a set of objects) using an assume-guarantee approach. A gas station system modeled with OBGGs is used to illustrate the contributions.This work is partially sponsored by projects IQ-MObile (CNPq-Brazil/CNR-Italy) and PLATUS (CNPq).Osmar Marchi dos Santos is partially sponsored by CAPES-Brazil.     

Formal Validation of a High Performance Error Control Protocol Using SPIN

This paper presents the specification and validation of a high performance error control protocol. A formal specification model of the protocol was described using the PROMELA language. Formal analysis of the protocol model was validated using the SPIN validation tool. The uncovering of several subtle properties of the protocol has demonstrated the advantage of employing formal validation methods in designing distributed systems.     

Verification support for ARINC‐653‐based avionics software

Software model checking consists in applying the most powerful results in formal verification research to programming languages such as C. One general technique to implement this approach is producing a reduced model of the software in order to employ existing and efficient tools, such as SPIN . This paper focusses on the application of this approach to the avionics software constructed on top of the Application Executive Software (APEX ) Interface, which is widely employed by manufacturers in the avionics industry. It presents a method to automatically extract PROMELA models from the C source code. In order to close the extracted model during verification, we built a reusable APEX ‐specific environment. This APEX environment models the execution engine (i.e. an APEX compliant real‐time operating system) that implements APEX services. In particular, it explains how to deal with aspects such as real‐time and APEX scheduling. Time is modelled in such a way that the we save time and memory by avoiding the analysis of irrelevant steps. This model of time and the construction of a deterministic scheduler guarantees the scalability of our approach. The paper also presents a tool that can verify realistic applications, and that has been used as a novel testing method to ensure the correctness of our APEX environment. This testing method uses SPIN to execute official APEX test cases. Copyright © 2010 John Wiley & Sons, Ltd.     

Alliance of model-driven engineering with a proof-based formal approach

Model-driven engineering (MDE) promotes the use of models throughout the software development cycle in order to increase abstraction and reduce software complexity. It favors the definition of domain-specific modeling languages (DSMLs) thanks to frameworks dedicated to meta-modeling and code generation like EMF (Eclipse Modeling Framework). The standard semantics of meta-models allows interoperability between tools such as language analysers (e.g., XText), code generators (e.g., Acceleo), and also model transformation tools (e.g., ATL). However, a major limitation of MDE is the lack of formal reasoning tools allowing to ensure the correctness of models. Indeed, most of the verification activities offered by MDE tools are based on the verification of OCL constraints on instances of meta-models. However, these constraints mainly deal with structural properties of the model and often miss out its behavioral semantics. In this work, we propose to bridge the gap between MDE and the rigorous world of formal methods in order to guarantee the correctness of both structural and behavioral properties of the model. Our approach translates EMF meta-models into an equivalent formal B specification and then injects models into this specification. The equivalence between the resulting B specification and the original EMF model is kept by proven design steps leading to a rigorous MDE technique. The AtelierB prover is used to guarantee the correctness of the model’s behavior with respect to its invariant properties, and the ProB model-checker is used to animate underlying execution scenarios which are translated back to the initial EMF model. Besides the use of these automatic reasoning tools in MDE, proved B refinements are also investigated in this paper in order to gradually translate abstract EMF models to concrete models which can then be automatically compiled into a programming language.

     

Petri网模型的扩展与检测

扩展了基本Petri网,提出了更加适合模型检测的MCPN方法,并将MCPN模型转换成模型检测工具SPIN的输入语言——PROMELA。使用SPIN完成对系统模型的检测,以提高软件设计的可靠性。在转换过程中,考虑了对当前情态下处于激活状态的多个变迁的同时激发;并提出了一种处理Petri网公平性问题的解决方案。     

PROMELA语义引擎执行研究

模型检查工具SPIN的核心是PROMELA语言,对PROMELA语言执行方式的理解决定所描述系统模型的行为方式。该文从语义角度研究了PROMELA语义引擎问题。首先给出PROMELA语法的抽象对象模型形式化定义,然后给出一个算法来实现PROMELA语法到抽象对象模型的映射,描述了PROMELA指称语义。     

Automatic Verification of a Behavioural Subset of UML Statechart Diagrams Using the SPIN Model-checker

Statechart Diagrams provide a graphical notation for describing dynamic aspects of system behaviour within the Unified Modelling Language (UML). In this paper we present a translation from a subset of UML Statechart Diagrams - covering essential aspects of both concurrent behaviour, like sequentialisation, parallelism, non-determinism and priority, and state refinement - into PROMELA, the specification language of the SPIN model checker. SPIN is one of the most advanced analysis and verification tools available nowadays. Our translation allows for the automatic verification of UML Statechart Diagrams. The translation is simple, proven correct, and promising in terms of state space representation efficiency. Received September 1999 / Accepted in revised form February 2000     

SynchRuler: a rule-based flexible synchronization model with model checking

Flexible synchronization models cannot provide a proper way of managing user interactions that change the course of a presentation. In this paper, we present a flexible synchronization model, termed SynchRuler, which allows such user interactions including backward and skip. The synchronization rules, which are based on event-condition-action (ECA) rules, are maintained to handle relationships among streams in SynchRuler. The synchronization rules are manipulated by the receiver-controller-actor (RCA) scheme, where receivers, controllers, and actors are objects to receive events, to check conditions, and to execute actions, respectively. The verification of a multimedia presentation specification is performed with the synchronization model. The correctness of the model and the presentation is controlled with a technique called model checking. Model checker PROMELA/SPIN tool is used for automatic verification of the correctness of LTL (linear temporal logic) formulas.     

An overview of model checking practices on verification of PLC software

Programmable logic controllers (PLCs) are heavily used in industrial control systems, because of their high capacity of simultaneous input/output processing capabilities. Characteristically, PLC systems are used in mission critical systems, and PLC software needs to conform real-time constraints in order to work properly. Since PLC programming requires mastering low-level instructions or assembly like languages, an important step in PLC software production is modelling using a formal approach like Petri nets or automata. Afterward, PLC software is produced semiautomatically from the model and refined iteratively. Model checking, on the other hand, is a well-known software verification approach, where typically a set of timed properties are verified by exploring the transition system produced from the software model at hand. Naturally, model checking is applied in a variety of ways to verify the correctness of PLC-based software. In this paper, we provide a broad view about the difficulties that are encountered during the model checking process applied at the verification phase of PLC software production. We classify the approaches from two different perspectives: first, the model checking approach/tool used in the verification process, and second, the software model/source code and its transformation to model checker’s specification language. In a nutshell, we have mainly examined SPIN, SMV, and UPPAAL-based model checking activities and model construction using Instruction Lists (and alike), Function Block Diagrams, and Petri nets/automata-based model construction activities. As a result of our studies, we provide a comparison among the studies in the literature regarding various aspects like their application areas, performance considerations, and model checking processes. Our survey can be used to provide guidance for the scholars and practitioners planning to integrate model checking to PLC-based software verification activities.     

Lightweight models for interpreting informal specifications

We explore the use of lightweight models, namely those in PROMELA/SPIN, by software engineers within the life cycle of software development. The primary goal is to improve the interpretation and understanding of an informal specification, not necessarily to validate the specification. We give details of an example involving an informal specification of an application protocol in telecommunications, namely the Request for Comments (RFC) standard for the Trivial File Transfer protocol (TFTP). We show how we were able to use this type of modelling in an iterative process, using tools that facilitate the process.     

LINUX进程间通信的模型检测

模型检测是一种强大的自动分析验证技术.分析了LINUX进程间通信的部分源代码并进行手工形式化建模,使用有限状态自动机描述模型,继而转换成SPIN的输入语言PROMELA,对其进行模型检测,验证了系统的有界性和可终止性,并就进程间通信中容易发生的问题提出了改进方案.     

Typical examples of using the atoment language

Atoment is a domain-specific language of executable specifications applied to describe methods and techniques of program verification. In this paper, a series of typical examples of using the Atoment language covering program models; the operational, transformational, and axiomatic semantics; and the formal specification of programming languages is presented.     

A design-oriented method to build correct hypermedia documents

Over the years, different approaches to identify temporal and spatial conflicts in hypermedia applications has been proposed. Most of them are based on formal verification techniques and impose to the designers to follow a formal model or language to ensure application’s functional correctness. Furthermore, the error diagnose is hard to be interpreted by a non-specialist in this domain. In this paper, we present an approach which supports formal verification for documents written in markup languages. We proposed a method and built a verification toolchain that helps designers to verify time and spatial constraints in hypermedia applications. The input language is the designer language. Its translation towards the input of toolchain is automatic and transparent for the application designer. The errors scenarios provided by the verification tool are presented in a timeline way, easily understandable by the designer. The method and toolchain support different markup languages translated in the same intermediary language in order to facilitate the use of different verification tools in the same environment.

     

Specification-driven model transformation testing

Testing model transformations poses several challenges, among them the automatic generation of appropriate input test models and the specification of oracle functions. Most approaches for the generation of input models ensure a certain coverage of the source meta-model or the transformation implementation code, whereas oracle functions are frequently defined using query or graph languages. However, these two tasks are usually performed independently regardless of their common purpose, and sometimes, there is a gap between the properties exhibited by the generated input models and those considered by the transformations. Recently, we proposed a formal specification language for the declarative formulation of transformation properties (by means of invariants, pre-, and postconditions) from which we generated partial oracle functions used for transformation testing. Here, we extend the usage of our specification language for the automated generation of input test models by SAT solving. The testing process becomes more intentional because the generated models ensure a certain coverage of the transformation requirements. Moreover, we use the same specification to consistently derive both the input test models and the oracle functions. A set of experiments is presented, aimed at measuring the efficacy of our technique.     

SEMANOL (73) a metalanguage for programming the semantics of programming languages

Summary SEMANOL is a practical programming system for writing readable formal specifications of the syntax and semantics of programming languages. SEMANOL is based on a theory of semantics which embraces algorithmic (operational) and extensional (input/output) semantics. Specifications for large contemporary languages have been constructed in the formal language, SEMANOL (73), which is a readable high-level notation. A SEMANOL (73) specification can be executed (by an existing interpreter program); when given a program from the specified language, and its input, the execution of the SEMANOL (73) specification produces the program's output. The demonstrated executability of SEMANOL (73) provides important practical advantages. This paper includes discussions of the theory of semantics underlying SEMANOL, the syntax and semantics of the SEMANOL (73) language, the use of the SEMANOL (73) language in the SEMANOL method for describing programming languages, and the contrast between the Vienna definition method (VDL) and SEMANOL.     

A generic framework: from modeling to code

Model-driven development (MDD) is a very popular technique in the area of software development, but this technique is criticized due to lack of a formal semantics. MDD is used for large-scale system development using semi-formal techniques like UML (Unified Modeling Language), which are not amenable to formal analysis and consistency checking. Formal methods with MDD may provide an assurance of correctness of the system. This paper advocates an approach to building generic framework for rigorous MDD that is based on combining semi-formal notations with formal modeling languages, correctness of the system using model checker and automatic code generation from the verified formal specification. The main objective of this work is to apply model-driven techniques and tools with formal verification and its code generation for designing critical systems. An assessment of the proposed framework is given through a case study, relative to the development of a cardiac pacemaker system.     

Automated verification of model transformations based on visual contracts

Model-Driven Engineering promotes the use of models to conduct the different phases of the software development. In this way, models are transformed between different languages and notations until code is generated for the final application. Hence, the construction of correct Model-to-Model (M2M) transformations becomes a crucial aspect in this approach. Even though many languages and tools have been proposed to build and execute M2M transformations, there is scarce support to specify correctness requirements for such transformations in an implementation-independent way, i.e., irrespective of the actual transformation language used. In this paper we fill this gap by proposing a declarative language for the specification of visual contracts, enabling the verification of transformations defined with any transformation language. The verification is performed by compiling the contracts into QVT to detect disconformities of transformation results with respect to the contracts. As a proof of concept, we also report on a graphical modeling environment for the specification of contracts, and on its use for the verification of transformations in several case studies.     

Prototyping realistic programming languages based on formal specifications

The specification of realistic programming languages is difficult and expensive. One approach to make language specification more attractive is the development of techniques and systems for the generation of language–specific software from specifications. To contribute to this approach, a tool–based framework with the following features is presented: It supports new techniques to specify more language aspects in a static fashion. This improves the efficiency of generated software. It provides powerful interfaces to generated software components. This facilitates the use of these components as parts of language–specific software. It has a rather simple formal semantics. In the framework, static semantics is defined by a very general attribution technique enabling e.g. the specification of flow graphs. The dynamic semantics is defined by evolving algebra rules, a technique that has been successfully applied to realistic programming languages. After providing the formal background of the framework, an object–oriented programming language is specified to illustrate the central specification features. In particular, it is shown how parallelism can be handled. The relationship to attribute grammar extensions is discussed using a non-trivial compiler problem. Finally, the paper describes new techniques for implementing the framework and reports on experiences made so far with the implemented system. Received: 20 November 1995 / 20 January 1997