Electronic Communications of the EASST (European Association of Software Science and Technology)
Not a member yet
887 research outputs found
Sort by
Teaching Modeling - An Initial Classification of Related Issues
Get PDFModeling is an important skill needed in both science and engineering domains. In software engineering, in particular, models are ubiquitous artefacts. The development, manipulation and understanding of models is therefore an important learning objective. The paper describes motivations and an outline of a research project aimed at classifying issues related to the teaching and learning of modeling together with some initial research results
Formal Specification and Verification of a Coordination Protocol for an Automated Air Traffic Control System
Get PDFSafe separation between aircraft is the primary consideration in air trafficcontrol. To achieve the required level of assurance for this safety-critical application,the Automated Airspace Concept (AAC) proposes three levels of conflict detectionand resolution. Recently, a high-level operational concept was proposed to definethe cooperation between components in the AAC. However, the proposed coordinationprotocol has not been formally studied. We use formal verification techniquesto ensure there are no potentially catastrophic design flaws remaining in the AACdesign before the next stage of production.We formalize the high-level operational concept, which was previously describedonly in natural language, in NuSMV and perform model validation by checkingagainst LTL/CTL specifications we derive from the system description. We writeLTL specifications describing safe system operations and use model checking forsystem verification. We employ specification debugging to ensure correctness ofboth sets of formal specifications and model abstraction to reduce model checkingtime and enable fast, design-time checking. We analyze two counterexamplesrevealing unexpected emergent behaviors in the operational concept that triggereddesign changes by system engineers to meet safety standards. Our experience reportilluminates the application of formal methods in real safety-critical system developmentby detailing a complete end-to-end design-time verification process includingall models and specifications
A Flattening Approach for Attributed Type Graphs with Inheritance in Algebraic Graph Transformation
Get PDFThe algebraic graph transformation approach was initiated in 1973 and supports the rule-based modification of graphs based on pushout constructions. The vertex and edge types used within the rules (or productions) as well as possible inheritance relationships defined between them are specified in the type graph. However, the termination proof can only be accomplished for graph transformation systems without inheritance relationships. Thus, all graph transformation systems with inheritance relationships in the type graph must be flattened. To this end, the algebraic graph transformation approach provides a formal description for how to flatten the type graph as well as a definition of abstract and concrete productions. In this paper, we will extend the definitions to also consider vertices in negative application conditions with finer node types and positive application conditions. Furthermore, we will prove the semantic equivalence of the original and the flattened graph transformation system. The whole flattening algorithm is then implemented in a prototype which supports an abstract or concrete flattening of a given graph transformation system. The prototype is finally evaluated within a case study
Process Evolution based on Transformation of Algebraic High-Level Nets with Applications to Communication Platforms
Get PDFAlgebraic High-Level (AHL) nets are a well-known modelling technique based on Petri nets with algebraic data types, which allows to model the communication structure and the data flow within one modelling framework. Transformations of AHL-nets – inspired by the theory of graph transformations – allow in addition to modify the communication structure. Moreover, high-level processes of AHL-nets capture the concurrent semantics of AHL-nets in an adequate way. In this paper we show how to model the evolution of communication platforms and scenarios based on transformations of algebraic high-level nets and processes. All constructions and results are illustrated by a running example showing the evolution of Apache Wave platforms and scenarios. The evolution of platforms is modelled by the transformation of AHL-nets and that of scenarios by the transformation of AHL-net processes.Our main result is a construction for the evolution of AHL-processes based on the evolution of the corresponding AHL-net. This result can be used to transform scenarios in a communication platform according to the evolution of possibly multiple actions of the platform
E-SPARK: Automated Generation of Provably Correct Code from Formally Verified Designs
Get PDFAn approach to generating provably correct sequential code from formallydeveloped algorithmic designs is presented. Given an algorithm modelledin the Event-B formalism, we automatically translate the design into the SPARKprogramming language. Our translation builds upon Abrial’s approach to the developmentof sequential programs from Event-B models. However, as well as generatingcode, our approach also automatically generates code level specifications, i.e.SPARK pre- and post-conditions, along with loop invariants. In terms of the SPARKproof tools, having the loop invariants increases verification automation. A prototype,known as E-SPARK, has been implemented as a plugin for the Rodin Platform(Event-B toolkit), and tested on a range of examples, i.e. searching, sorting andnumeric calculations
Semantic Adaptation using CCSL Clock Constraints
Get PDFWhen different parts of a system depend on different technical domains, the best suitable paradigm for modeling each part may differ. In this paper, we focus on the semantic adaptation between parts of a model which use different modeling paradigms in the context of model composition. We show how CCSL, a language for defining constraints and relations on clocks, can be used to define this semantic adaptation in a formal and modular way
Threshold Concepts in Object-Oriented Modelling
Get PDFProponents of the object-oriented (OO) paradigm frequently claim that the OO paradigm is ‘more natural’ than the procedural paradigm because the world is filled with objects that have both attributes and behaviors. However students in higher education generally experience considerable difficulty in understanding OO concepts and acquiring the necessary skills in object-oriented analysis and design. This paper proposes OO modelling to be a set of threshold concepts and describes a study that sought to improve undergraduate students’ learning of OO modelling by adopting concept maps as ‘stepping stones’ to facilitate the development of analysis class and sequence diagrams
Optimizing Model-Based Software Product Line Testing with Graph Transformations
Get PDFSoftware Product Lines (SPLs) are increasing in relevance and importance as various domains strive to cope with the challenges of supporting a high degree of variability in modern software systems. Especially the systematic testing of SPLs is non-trivial as a high degree of variability implies a vast number of possible products.As testing every valid product individually quickly becomes infeasible, heuristics are often used to choose a representative subset of products to be tested. MoSo-PoLiTe (Model-Based Software Product Line Testing) is a framework for SPL testing that combines and applies combinatorial (in particular pairwise) and model-based testing to SPL feature models. In this paper, we (1) present MoSo-PoLiTe as a novel case study for graph transformations in general and Story Driven Modelling (SDM) in particular, (2) show why we consider SDMs to be ideal for rapid prototyping optimization strategies in this context, and (3) evaluate our implemented optimizations and quantify the realized improvements for MoSo-PoLiTe
Language Evolution, Metasyntactically
Get PDFCurrently existing syntactic definitions employ many different notations (usually dialects of EBNF) with slight deviations among them, which prevent efficient automated processing. When changes in such notation are required either due to maintenance activities such as correction or evolution, or because a grammar collection is written in a different notation than the one required by the grammarware toolkit, we speak of metalanguage evolution: i.e., a special language evolution scenario when the language itself does not necessarily evolve, but the notation in which it is written, does. Notational changes need to be propagated to different levels, such as to parsers that used to work with the old notation, to grammars of those notations that served as explanation material, and to the existing grammarbase.The solution proposed in this paper, relies on composing a notation specification and expressing notation changes as transformations of that specification. These transformation steps are coupled to changes in the notation grammar (i.e., grammar for grammars) and to changes in other grammars written in the original notation. This paper explains the general setup of such an infrastructure, with links to the prototypical implementation of the solution
Multi-core and/or Symbolic Model Checking
Get PDFWe review our progress in high-performance model checking. Our multi-core model checker is based on a scalable hash-table design and parallel random-walk traversal. Our symbolic model checker is based on Multiway Decision Diagrams and the saturation strategy. The LTSmin tool is based on the PINS architecture, decoupling model checking algorithms from the input specification language. Consequently, users can stay in their own specification language and postpone the choice between parallel or symbolic model checking. We support widely different specification languages including those of SPIN (Promela), mCRL2 and UPPAAL (timed automata). So far, multi-core and symbolic algorithms had very little in common, forcing the user in the end to make a wise trade-off between memory or speed. Recently, however, we designed a novel multi-core BDD package called Sylvan. This forms an excellent basis for scalable parallel symbolic model checking