Electronic Communications of the EASST (European Association of Software Science and Technology)
Not a member yet
887 research outputs found
Sort by
Experiences in the Industrial use of Formal Methods
Get PDFAltran Praxis has used formal methods within its high integrity development approach, Correctness by Construction (CbyC), for a number of years. The Tokeneer ID Station (TIS) developed for the US National Security Agency (NSA) is one example of a development using formal methods and the CbyC approach. This project used a number of rigorous techniques including formalisation of the specification using the Z Notation, refinement of the specification to a formal design, software development in SPARK with proof of absence of run-time errors of the software and proof of system properties. The project has stood up well to the intense scrutiny it has been subject to since it became available to the wider community in 2008, with only five errors being found. Despite the general success of the approach there are challenges to using formal methods in an industrial context. By looking at a number of key properties that affect the success of deployment of tools and techniques in industry we attempt to put the challenges of industrial deployment of formal methods into perspective
Minimizing Finite Automata with Graph Programs
Get PDFGP (for Graph Programs) is a rule-based, nondeterministic programming language for solving graph problems at a high level of abstraction, freeing programmers from dealing with low-level data structures. In this case study, we present a graph program which minimizes finite automata. The program represents an automaton by its transition diagram, computes the state equivalence relation, and merges equivalent states such that the resulting automaton is minimal and equivalent to the input automaton. We illustrate how the program works by a running example and argue that it correctly implements the minimization algorithm of Hopcroft, Motwani and Ullman. We also prove a quadratic upper bound for the number of rule schema applications used by the program
Realizing Impure Functions in Interaction Nets
Get PDFWe propose and illustrate first steps towards an extension of
interaction nets based on monads to handle functions with side effects
(e.g., I/O, exceptions). We define three monads for common types of side effects
and show their correctness by proving the monad laws
Formal Specification of Model Transformations by Triple Graph Grammars with Application Conditions
Get PDFTriple graph grammars are a successful approach to describe exogenous model transformations, i.e. transformations between models conforming to different meta-models. Source and target models are related by some connection part, triple rules describe the simultaneous construction of these parts, and forward and backward rules can be derived modeling the forward and backward model transformations.
As shown already for the specification of visual models by typed attributed graph transformation, the expressiveness of the approach can be enhanced significantly by using application conditions, which are known to be equivalent to first order logic on graphs.
In this paper, we extend triple rules with a specific form of application conditions, which enhance the expressiveness of formal specifications for model transformations. We show how to extend results concerning information preservation, termination, correctness, and completeness of model transformations to the case with application conditions. We illustrate our approach and results with a model transformation from statecharts to Petri nets
Proving Distributed Algorithms by Combining Refinement and Local Computations
Get PDFDistributed algorithms are considered to be very complex to design and to prove; our paper contributes to the design of correct-by-construction distributed algorithms. The main idea relies upon the development of distributed algorithms following a top/down approach, which is clearly well known in earlier works of Dijkstra, and to use refinement for proving the correctness of the resulting algorithms. However, the link between the problem and the first model remains to be expressed and the refinement is a real help to justify in a very progressive way the choices of design. We propose in this work a framework combining local computations models
and refinement to prove the correctness of a large class of distributed algorithms. Local computations models define abstract computing processes for solving problems by distributed algorithms and can be integrated into a the Event-B modelling language
to define proof-based patterns for the design of distributed algorithms. We illustrate our approach by examples like the leader election protocol or the distributed coloring algorithm. Our proposal is integrated into an environment called ViSiDiA
Development of Rabin’s Choice Coordination Algorithm in Event-B
Get PDFThe paper reports our investigation on tool support for the integration of qualitative probabilistic reasoning into Event-B. In the process, we formalise a non- trivial algorithm, namely Rabin’s choice coordination. Our correctness reasoning is a combination of termination proofs in terms of probabilistic convergence and standard invariant techniques. Moreover, we describe how qualitative probabilistic reasoning can be maintained during refinement
Position Paper: m2n—A Tool for Translating Models to Natural Language Descriptions
Get PDFTo describe the structure of a system, the UML Class Diagram yields the means-of-choice. Therefor, the Class Diagram provides concepts like class, attribute, operation, association, generalization, aggregation, enumeration, etc. When students are introduced to this diagram, they often have to solve exercises where texts in natural language are given and they have to model the described systems. When analyzing such exercises, it becomes evident that certain kinds of phrases describing a particular concept appear again and again contextualized to the described domain.
In this paper, we present an approach which allows the automatic generation of textual specifications from a given Class Diagram based on standard phrases in natural language. Besides supporting teachers in preparing exercises, such an approach is also valuable for various e-learning scenarios
Extending ASSL: Making UML Metamodel-based Workflows executable
Get PDFASSL is a language that enables UML developers to test and certify UML and OCL models [5]. Snapshots of system states are semi-automatically created and main parts of the UML action semantics is implemented by the language. Its interpreter is the well-known UML modeling tool USE. The article proposes a number of language extensions to ASSL. These include (sub ) procedure calls and pre- and postcondition checks on entering and exiting of operations using OCL. The paper motivates the need for these extensions as well as their usage and development along the problem of metamodel-based execution of workflow models. Executable workflow models, driven by ASSL procedures, are introduced in detail to present the usage of ASSL and our extensions
Generating Instance Graphs from Class Diagrams with Adaptive Star Grammars
Get PDFIn model-driven software engineering, class diagrams are used to define the structure of object-oriented software and valid object configurations, i.e., what objects may occur in a program and how they are related. Object configurations are essentially graphs, so that class diagrams define graph languages. Class diagrams are declarative, i.e., it is quite easy to check whether a graph is an instance of a class diagram. Graph grammars, on the other hand, define a graph language by derivation and are thus well suited for constructing instance graphs. This paper describes how a class diagram can be translated into a graph grammar that defines the same graph language as the original class diagram. Such a graph grammar may then be used for, e.g., automatically generating valid object configurations as test cases. In contrast to earlier attempts, the presented approach allows to translate class diagrams with arbitrary multiplicities, unique and non-unique associations, composition associations, class generalization, association subsetting and redefinition. This is made possible by using adaptive star grammars, a special kind of graph grammars
Local Confluence Analysis of Consistent EMF Transformations
Get PDFModel transformation is one of the key activities in model-driven software development. An increasingly popular technology to define modeling languages is provided by the Eclipse Modeling Framework (EMF). Several EMF model transformation approaches have been developed, focusing on different transformation aspects. For the analysis of model transformations, graph transformation techniques provide a formal basis and tool support. In this paper we aim to make use of those techniques by providing a formal foundation of consistent EMF transformations to analyze critical pairs between EMF transformation rules as well as extending the notion of local confluence to EMF transformation systems. The analysis is also demonstrated on a small example simulating the firing behavior of elementary Petri nets