Electronic Communications of the EASST (European Association of Software Science and Technology)
Not a member yet
887 research outputs found
Sort by
Semi-automatic Proofs about Object Graphs in Separation Logic
Get PDFPublished correctness proofs of garbage collectors in separationlogic to date depend on extensive manual, interactive formulamanipulations. This paper shows that the approach of symbolicexecution in separation logic, as first developed by Smallfoot,also encompasses reasoning about object graphs given by the reachabilityof objects. This approach yields semi-automatic proofs oftwo central garbage collection algorithms: Schorr-Waite graph marking and Cheney's collector. Our framework is developed as a conservativeextension of Isabelle/HOL. Our verification environment re-uses theSimpl framework for classical Hoare logic
Remedy of Mixed Initiative Conflicts in Model-based System Engineering
Get PDFSPACE is a technique for model-driven engineering of reactive distributedsystems. One of the strengths of its tool-set Arctis is that the system engineercan formally analyze the models for design errors such that these can becorrected early in the development process. In this paper, we go a step further andintroduce a technique that refines the fault detection and, in addition, offers a highlyautomatic mechanism to remedy the errors. For that, we combine model checking,the already existing analysis method of Arctis, with graph transformation. Usinggraph rewriting rules, we can analyze the state space graph of a system for the exact reason of an error as well as remove the erroneous parts of a model by changing themodel description. We exemplify the approach by envisaging the detection and remedyof mixed initiatives, a quite common cause for faulty behavior in event-drivensystems that often is overlooked in system development
Model Correctness Patterns as an Educational Instrument
Get PDFUML class diagrams play a central role in modeling activities. Given the difficulty in producing high quality models, modelers must be equipped with an awareness of model design problems and the ability to identify and correct such models. In this paper we observe the role of class diagram correctness patterns as an educational instrument for improving class diagram modeling. We describe a catalog of correctness and quality design (anti)-patterns for class diagrams. The patterns characterize problems, analyze their causes and provide repairing advice. Pattern specification requires an enhancement of the class diagram meta-model. The pattern classification has a major role in clarifying design problems. Finally, we describe an actual experiment of using the catalog for teaching modeling
Model Checking Algorithms for Markov Automata
Get PDFMarkov automata constitute a compositional modeling formalism spanning as special cases the models of discrete and continuous time Markov chains, as well as interactive Markov chains and probabilistic automata. This paper discusses the core algorithmic ingredients of a numerical model checking procedure for Markov automata with respect to a PCTL or CSL like temporal logic. The main challenge lies in the computation of time-bounded reachability probabilities, for which we provide a stable approximation scheme
Asserting the Correctness of Software Language Translations
Get PDFWhile building a new language, we assign its semantics by mapping its syntax onto a semantic domain. To do so, we can either (i) do it operationally, by means of small-step morphisms within the same semantic-domain; or (ii) by means of a translation (syntax-to-syntax transformation), onto a target language that has already an operational semantics defined. Despite the fact that it is possible to build the set of syntactic correspondences from a given translation, it is still not clear how we can assert about the correctness of these syntactic correspondences in w.r.t. both the source and target language's underlying semantics.In this paper, we combine the above described techniques by analyzing the translation and establishing a semantic relation between the respective operational semantics, in order to assert the correctness of that translation. We demonstrate our approach with a concrete translation between two languages: State Machines and Petri Nets; and decide about its correctness by using their respective operational semantics as oracles. Finally, we discuss about the validity of our assertions in w.r.t. language translations in general
Verifying Access Control in Statecharts
Get PDFAccess control is one of the main security mechanisms for software applications. It ensures that all accesses conform to a predefined access control policy. It is important to check that the access control policy is well implemented in the system. When following an MDD methodology it may be necessary to check this early during the development lifecycle, namely when modeling the application. This paper tackles the issue of verifying access control policies in statecharts. The approach is based on the transformation of a statechart into an Algebraic Petri net to enable checking access control policies and identifying potential inconsistencies with an OrBAC set of access control policies. Our method allows locating the part of the statechart that is causing the problem. The approach has been successfully applied to a Library Management System. Based on our proposal a tool for performing the transformation and localization of errors in the statechart has been implemented
Adding Rule-Based Model Transformation to Modelling Languages in MetaEdit+
Get PDFMetaEdit+ is a commercial tool by MetaCase for creating domain-specific, syntax-directed visual modelling environments. MetaEdit+ synthesizes such environments from user-provided metamodels and contains a Generator Editor for code/report generation. An API is provided to allow external manipulation of models through SOAP. Currently, the MetaEdit+ tool does not natively support rule-based model-to-model transformation. Such transformations are useful as they allow domain experts to intuitively (using domain-specific notations) model either operational semantics (a simulator) or denotational semantics (through model-to-model transformation onto a model in a known formalism) of a modelling language. We will demonstrate how to add rule-based operational semantics to modelling languages in MetaEdit+. In our approach, transformation rules are visually created in MetaEdit+. The rule editor is synthesized using modified versions of the original language's metamodel. This modification is performed in a structured fashion using a process called RAMification. Both the model and the rules are exported from MetaEdit+ to Python code. This code is combined with Py-T-Core, our library of transformation language primitives, to apply the rules on the model. Our demonstration has a client-server architecture, with the MetaEdit+ visual modelling environment as the client and the transformation engine as the server. After each transformation step, in-place changes to the model are propagated to MetaEdit+ for visualization using the SOAP API. A simple (manufacturing) Production System modelling language is used as an example
Avoiding OCL specification pitfalls
Get PDFThis paper discusses about teaching software modeling by using OCL specifications, in the context in which the web represents the main source of information. The raise of the interest for models induced a higher need for clear and complete specifications. In case of models specified by means of MOF-based languages, adding OCL constraints proved to be an interesting answer to this need. Several OCL examples posted on web include hasty specifications, that are often dissuasive with respect to complementing models with OCL specification. OCL beginners, and not only, need to know how to avoid potential specification traps.Our proposal is based on a complete and unambiguous description of requirements, that represents the first step towards good OCL specifications. The work highlights several major aspects that need to be understood and complied with to produce meaningful and efficient OCL specifications. This approach was tested while teaching OCL at Babes-Bolyai University of Cluj-Napoca
Gray Box Coverage Criteria for Testing Graph Pattern Matching
Get PDFModel transformations (MT) are a core building block of Model-Driven Engineering. The quality of MT specifications and implementations is vital to their success. The well-researched formal underpinning of graph transformation (GT) theory allows for proving quality-relevant properties and enables stringent implementations. Yet, in practice, MT implementations often depend on verification/validation techniques based on dynamic testing. This work presents a new gray box coverage approach for systematic testing of GT-based MT implementations and pattern specifications. The approach uses GT specifics and enforces systematic testing by examining variable binding and unbinding steps, thereby not making further assumptions about the underlying pattern matching algorithm. A family of coverage criteria is defined as temporal logic (LTL) formulae, and the effectiveness of concrete criteria in limiting the testing effort is examined by an example