Electronic Communications of the EASST (European Association of Software Science and Technology)
Not a member yet
887 research outputs found
Sort by
Algebraic Approach to Timed Petri Nets
Get PDFOne aspect often needed when modelling systems of any kind is time-based analysis, especially for real-time or in general time-critical systems. Algebraic place/transition (P/T) nets do not inherently provide a way to model the passing of time or to restrict the firing behaviour with regards to passing time. In this paper, we present an extension of algebraic P/T nets by adding time durations to transitions and timestamps to tokens. We define categories for different timed net classes and functorial relations between them. Our first result is the definition of morphisms preserving firing behaviour for all timed net classes. As second result, we define structuring techniques for timed P/T nets in a way that our category fulfills the properties of M-adhesive systems, a general categorical framework for structuring and transforming high-level algebraic structures. We demonstrate our approach by applying it to model a real-time communication network
7th International Workshop on Graph Based Tools (GraBaTs 2012): Preface
Get PDFThe 7th International Workshop on Graph Based Tools is the continuation of the GraBaTs series of workshops which provides a forum for researchers and practitioners interested in the development and application of graph-based tools. The purpose of this workshop is to survey the state of the art of graph-based tools, bring together developers of graph-based tools in different application fields and to encourage new tool development cooperations. GraBaTs 2012 is the 7th edition in a line of workshops which started 10 years ago at ICGT'02
Automated Verification of Specifications with Typestates and Access Permissions
Get PDFWe propose an approach to formally verify Plural specifications of concurrent programs based on access permissions and typestates, by model-checking automatically generated abstract state-machines. Our approach captures all possible relevant behaviors of abstract concurrent programs implementing the specification. We describe the formal methodology employed in our technique and provide an example as proof of concept for the state-machine construction rules. We implemented the fully automated algorithm to generate and verify models as a freely available plug-in of the Plural tool, called Pulse. We tested Pulse on the full specification of a Multi Threaded Task Server commercial application and showed that this approach scales well and is efficient in finding errors in specifications that could not be previously detected with the Data Flow Analysis (DFA) capabilities of Plural
Proceedings of the 11th International Workshop on Graph Transformation and Visual Modeling Techniques
Get PDF
Symbolic Model Checking and Safety Assessment of Altarica models
Get PDFAltarica is a language used to describe critical systems. In this paper we present a novel approach to the analysis of Altarica models, based on a translation into an extended version of NuSMV. This approach opens up the possibility to carry out functional verification and safety assessment with symbolic techniques. An experimental evaluation on a set of industrial case studies demonstrates the advantages of the approach over currently available tools.
ReConNet: A Tool for Modeling and Simulating with Reconfigurable Place/Transition Nets
Get PDFIn this contribution we present a tool for modeling and simulation with reconfigurable Petri nets. Taking the idea of algebraic graph transformations to marked Petri nets we obtain Petri nets whose net structure can be changed dynamically. The rule-based change of the net structure enables the adequate modeling of complex, dynamic structures as for example of the scenarios of the Living Place Hamburg. The tool \reconnet \ uses decorated place/transition nets that are extended by various annotations. Especially, they have transition labels that may change when the transition fires. The transformation approach is based on the well-known algebraic transformation approach, but here we use a variant, namely the cospan approach, that inverts the relation between left- and right-hand sides and interface in the rules
Complex Attribute Manipulation in TGGs with Constraint-Based Programming Techniques
Get PDFModel transformation plays a central role in Model-Driven Engineering (MDE) and providing bidirectional transformation languages is a current challenge with important applications. Triple Graph Grammars (TGGs) are a formally founded, bidirectional model transformation language shown by numerous case studies to be quite promising and successful. Although TGGs provide adequate support for structural aspects via object patterns in TGG rules, support for handling complex relationships between different attributes is still missing in current implementations. For certain applications, such as bidirectional model-to-text transformations, being able to manipulate attributes via string manipulation or arithmetic operations in TGG rules is vital. Our contribution in this paper is to formalize a TGG extension that provides a means for complex attribute manipulation in TGG rules. Our extension is compatible with the existing TGG formalization, and retains the "single specification'' philosophy of TGGs
Relating Algebraic and Coalgebraic Descriptions of Lenses
Get PDFLenses are a heavily studied form of bidirectional transformation, with diverse applications including database view updating, software development and memory management. Previous work has explored lenses category-theoretically, and established that the category of lenses for a fixed "view" V is, up to isomorphism, the category of algebras for a particular monad on Set/V. It has recently been shown that lenses are the coalgebras for the comonad generated by the cartesian closure adjunction on Set. In this paper, we present an equational proof of the coalgebra correspondence, note that the algebra correspondence extends to arbitrary categories with products and that the coalgebra correspondence extends to arbitrary cartesian closed categories, and show that both correspondences extend to isomorphisms of categories. The resulting isomorphism between a category of algebras and a category of coalgebras is unexpected, and we analyze its underlying generality and the particularity that restricts its applicability. We end with remarks about the utility of the two different treatments of lenses, especially for obtaining further, more realistic, generalizations of the notion of lens
On the Unification of Megamodels
Get PDFThrough the more and more widespread application of model-driven engineering (MDE) and the increasing diversity in applied modeling paradigms within single projects, there is an increasing need to capture not only models in isolation but also their relations.This paper is a survey on techniques capturing such relations, such as megamodels or macromodels, based on existing scientific literature. Therefore, we consider various definitions of these techniques. We further examine characteristics of the different techniques.We will propose a unified core definition of a megamodel that captures the core properties of megamodels and which can be extended to the needs of the different applications of megamodels.Finally, we give an outlook on arising application areas for megamodels