Electronic Communications of the EASST (European Association of Software Science and Technology)
Not a member yet
887 research outputs found
Sort by
Instance Generation from Type Graphs with Arbitrary Multiplicities
Get PDFMeta modeling is a wide-spread technique to define visual languages, with the UML being the most prominent one. Despite several advantages of meta modeling such as ease of use, the meta modeling approach has a major disadvantage: It does not offer a direct means for generating its language elements. This disadvantage poses a severe limitation on certain applications. For example, when developing model transformations, it is desirable to have enough valid instance models available for large-scale testing. Producing such a large set by hand is tedious. In the related problem of compiler testing, a string grammar together with a simple generation algorithm is typically used to produce words of the language automatically. In this paper, we formalize a restricted form of meta-models by type graphs with multiplicities and introduce instance-generating graph grammars for creating instance graphs representing the abstract syntax structures of models. Thereby, a further step is taken to overcome the main deficit of the meta-modeling approach
Towards Alternating Automata for Graph Languages
Get PDFIn this paper we introduce alternating automata for languages of arrows of an arbitrary category, and as an instantiation thereof alternating automata for graph languages. We study some of their closure properties and compare them, with respect to expressiveness, to other methods for describing graph languages. We show, by providing several examples, that many graph properties (of graphs of bounded path width) can be naturally expressed as alternating automata
Harnessing SMT Solvers for TLA+ Proofs
Get PDFTLA+ is a language based on Zermelo-Fraenkel set theory and linear temporal logic designed for specifying and verifying concurrent and distributed al- gorithms and systems. The TLA+ proof system TLAPS allows users to interactively verify safety properties of these systems. At the core of TLAPS, a proof manager interprets the proof language, generates corresponding proof obligations and passes them to backend provers. We recently developed a backend that relies on a typing discipline to encode (untyped) TLA+ formulas into multi-sorted first-order logic for SMT solvers. In this paper we present a different encoding of TLA+ formulas that does not require explicit type inference for TLA+ expressions. We also present a number of techniques based on rewriting in order to simplify the resulting formulas
Specification and refinement of discrete timing properties in Event-B
Get PDFEvent-B is a formal language for systems modeling, based on set theoryand predicate logic. It has the advantage of mechanized proof, and it is possible tomodel a system in several levels of abstraction by using refinement. Discrete timingproperties are important in many critical systems. However, modeling of timingproperties is not directly supported in Event-B. In this paper we identify three maincategories of discrete timing properties for trigger-response pattern, deadline, delayand expiry. We introduce language constructs for each of these timing properties thataugment the Event-B language. We describe how these constructs can be mappedto standard Event-B constructs. To ease the process of using the timing constructsin a refinement-based development, we introduce patterns for refining the timingconstructs that allow timing properties on abstract models to be replaced by timingproperties on refined models. The language constructs and refinement patternsare illustrated through some generic examples. Event-B refinement allows atomicevents at the abstract level to be broken down into sub-steps at the refined level.The goal of our refinement patterns is to provide an easy way to represent and correctlyrefine timing constraints on abstract atomic events with more elaborate timingconstraints on the refined events. This paper presents an initial set of patterns
Automatic Deployment Space Exploration Using Refinement Transformations
Get PDFTo manage the complex engineering information for real-time systems, the system under development may be modelled in a high-level architecture de- scription language. This high-level information provides a basis for deployment space exploration as it can be used to generate a low-level implementation. During this deployment mapping many platform-dependent choices have to be made whose consequences cannot be easily predicted. In this paper we present an approach to the automatic exploration of the deployment space based on platform-based design. All possible solutions of a deployment step are generated using a refinement trans- formation. Non-conforming deployment alternatives are pruned as early as possible using simulation or analytical methods. We validate the feasibility of our approach by deploying part of an automotive power window optimized for its real-time be- haviour using an AUTOSAR-like representation. First results are promising and show that the optimal solution can indeed be found efficiently with our approach
Recent Advances in Multi-Paradigm Modeling
Get PDFFollowing the trend of other editions, it was held this year (2011) in Wellington, New Zealand, the 5th International Workshop on Multi-Paradigm Modelling: Concepts and Tools (MPM). Once again has been a satellite event of the International Conference on Model-Driven Engineering Languages and Systems (MoDELS). It aims at further the state-of-the-art as well as to define future directions of this emerging research area by bringing together world experts in the field for an intense one-day workshop. This paper summarizes the results of this year's event
Optimized Transformation and Verification of SystemC Methods
Get PDFConcurrent designs can be automatically verified by transforming them into an automata-based representation and by model checking the resulting model. However, when transforming a concurrent design into an automata-based representation, each method has to be translated into a single automaton. This produces a significant overhead for model checking. In this paper, we present an optimization of our previously proposed transformation from SystemC into Uppaal timed automata. The main idea is that we analyze whether SystemC methods can be executed atomically and then we use the results for generating a reduced automata model. We have implemented the optimized transformation in ourSystemC to Timed Automata Transformation Engine (STATE) and demonstrate the effect of our optimization with experimental results from micro benchmarks, a simple producer-consumer example, and from an Anti-Slip Regulation and Anti-lock Braking System (ASR/ABS)
Visual Modeling and Analysis of EMF Model Transformations Based on Triple Graph Grammars
Get PDFThe tool HENSHIN is an Eclipse plug-in supporting visual modeling and execution of rule-based EMF model transformations. This paper describes the recent extensions of HENSHIN by a visual editor for triple graph grammars (TGGs).The visual editor (called HENSHINTGG) supports a compact visualization of triple rules in an integrated editor panel. Internally, triple graph rules are represented as HENSHIN rules and can be simulated using the HENSHIN EMF model transformation engine. Our extension supports the automatic generation of forward translation rules for transforming source into target models. A converter from HENSHIN TGG rules to the graph transformation analysis tool AGG allows a systematic check for conflicts of forward translation rules in AGG based on critical pair analysis
Combining Model Checking and Discrete-Event Supervisor Synthesis
Get PDFWe present an approach to facilitate the design of provably correct concurrent systems by recasting recent work that uses discrete-event supervisor synthesis to automatically generate concurrency control code in Promela and combine it with model checking in Spin. This approach consists of the possibly repeated execution of three steps: manual preparation, automatic synthesis, and semi-automatic analysis. Given a concurrent Promela program C devoid of any concurrency control and an informal specification E_in , the preparation step is assumed to yield a formal specification E of the allowed system behaviours and two versions of C: C_e to identify the specification-relevant events in C and enable supervisor synthesis, and C_e,a to introduce “checkable redundancy” and used during the analysis step to locate bugs in: the specification formalization E, the event markup in C_e, or the implementation of the synthesis. The result is supervised Promela code C_sup that is more likely to be correct with respect to E and E_in. The approach is illustrated with an example. A prototype tool implementing the approach is described
Position Paper: Software Modeling Education
Get PDFModel-driven engineering (MDE) is a promising paradigm to deal with the ever increasing complexity of modern software systems. Its powerful abstraction mechanisms allow practitioners to focus on the essential development challenges, thereby hiding the irrelevant aspects of the system under development. Within the last few years, noticeable progress has been made in putting MDE into practice,particularly in those areas where the activity of programming is substituted by modeling. The recent availability of matured concepts and stable tools has resulted in MDE becoming more applicable in software engineering projects. Nevertheless, the availability of the best technology is worthless, if it is not accepted and used by practitioners in the field. To alleviate this problem there is a need for extensive training both in academia and industry to fully exploit the power of MDE.In this paper, we discuss the efforts being undertaken in the educational communities to promote the application of modeling and MDE technologies and discuss several challenges which still need to be addressed