Electronic Communications of the EASST (European Association of Software Science and Technology)
Not a member yet
887 research outputs found
Sort by
Preface
Get PDFPreface of the Proceedings of the Fourth International Workshop on Petri Nets and Graph Transformation PNGT 201
Automated Support for the Design and Validation of Fault Tolerant Parameterized Systems: a case study
Get PDFWe propose a methodology to use the infinite state model checker MCMT, based on Satisfiability Modulo Theory techniques, for assisting in the design of fault tolerant algorithms. To prove the practical viability of our methodology, we apply it to formally check the agreement property of the reliable broadcast protocols of Chandra and Toueg
Categorical Abstract Rewriting Systems and Functoriality of Graph Transformation
Get PDFAbstract rewriting systems are often defined as binary relations over a given set of objects. In this paper, we introduce a new notion of abstract rewriting system in the framework of categories. Then, we define the functoriality property of rewriting systems. This property is sometimes called vertical composition. We show that most graph transformation systems are functorial and provide a counter-example of graph transformation system which is not functorial
Coinductive Graph Representation: the Problem of Embedded Lists
Get PDFWhen trying to obtain formally certified model transformations, one may want to represent models as graphs and graphs as greatest fixed points. To do so, one is rather naturally led to define co-inductive types that use lists (to represent a finite but unbounded number of children of internal nodes). These concepts are rather well supported in the proof assistant Coq. However, their use in our intended applications may cause problems since the co-recursive call in the type definition occurs in the list parameter. When defining co-recursive functions on such structures, one will face guardedness issues, and in fact, the syntactic criterion applied by the Coq system is too rigid here.
We offer a solution using dependent types to overcome the guardedness issues that arise in our graph transformations. We also give examples of further properties and results, among which finiteness of represented graphs. All of this has been fully formalized in Coq
Modelling Distributed Cognition Systems in PVS
Get PDFWe report on our efforts to formalise DiCoT, an informal structured approach for analysing complex work systems, such as hospital and day care units, as distributed cognition systems. We focus on DiCoT's information flow model, which describes how information is transformed and propagated in the system. Our contribution is a set of generic models for the specification and verification system PVS. The developed models can be directly mapped to the informal descriptions adopted by human-computer interactions experts. The models can be verified against properties of interest in the PVS theorem prover. Also, the same models can be simulated, thus facilitating analysts to engage with stakeholders when checking the correctness of the model. We trial our ideas on a case study based on a real-world medical system
Neighbourhood Abstraction in GROOVE
Get PDFImportant classes of graph grammars have infinite state spaces and therefore cannot be verified with traditional model checking techniques. One way to address this problem is to perform graph abstraction, which allows us to generate a finite abstract state space that over-approximates the original one. In previous work we developed the theory of neighbourhood abstraction. In this paper, we present the implementation of this theory in GROOVE and illustrate its use with a small grammar that models operations on a single-linked list
OCL Tools Report based on the IDE4OCL Feature Model
Get PDFPreviously we have developed the idea of an Integrated Development Environment for OCL (IDE4OCL). Based on the OCL community's feedback we have also designed and published an IDE4OCL feature model. Here we present a report on selected OCL tools developed by the authors and their teams. Each author gives an overview of their OCL tool, provides a top level architecture, and gives an evaluation of the tool features in a web framework. The framework can also be used by other potential OCL users and tool developers. For users it may serve as an aid to choose a suitable tool for their OCL use scenarios. For tool developers it provides a comparative view for further development of the OCL tools. Our plans are to maintain the collected data and extend this web framework by further OCL tools. Additionally, we would like to encourage sharing of OCL development resources
Verification of Model Transformations to Refactoring Mobile Social Networks
Get PDFVerification of model processing programs, where only the definitions of the program and the languages of the models to be transformed are analyzed, has become a fundamental issue in model-based software engineering. This analysis may become very complex, but it is performed only once and the results are independent from concrete input models. The formal background of verification methods for graph rewriting-based model transformations has become a subject of research recently. In previous work, we have provided fundamental formal and algorithmic background of a (semi-)automated verification approach for graph transformations. This work concludes these components and put them together to introduce the implementation of a verification system fully integrated into a model transformation framework, VMTS. The strong points of our approach is its usability, its implementation in an existing tool, and its extendibility, which are demonstrated on a case study in the application domain of mobile centric social networks. Our results show that the verification of graph rewriting-based model transformations can be largely automated
Modelling Emergency Scenarios using Algebraic High Level Net Transformation Systems with Net Patterns
Get PDFEmergency operations are a good case study for dynamic systems. Their
size and high dynamicity make modelling them a challenging task. Algebraic high
level net transformation systems are a well suited technique for modelling such dynamic
systems. They consist of an algebraic high level net and a set of graph transformation
rules. The net reflects the initial state of the operation and the transformation
rules can be used to adapt this state to reflect the dynamicity of the operation.
The applicability of graph transformation rules depends on the existence of a match
morphism. While designing the algebraic high level net transformation system the
designer has to ensure the existence of the right match morphisms for all reachable
runtime states. This can be a tedious and error prone task for the designer. This
paper uses a case study for modelling emergency operations with algebraic high
level net transformation systems to show how the notion of net patterns can help the
designer to cope with rule applicability