Electronic Communications of the EASST (European Association of Software Science and Technology)
Not a member yet
887 research outputs found
Sort by
Attribute Handling for Bidirectional Model Transformations: The Triple Graph Grammar Case
Get PDFWhen describing bidirectional model transformations in a declarative (relational) way, the relation between structures in source and target models is specified. But not only structural correspondences between source and target models need to be described. Another important aspect is the specification of the relation between attribute values of elements in source and target models. However, most existing approaches either do not allow such a relational kind of specification for attributes or allow it only in a restricted way.We consider the challenge of bridging the gap between a flexible declarative attribute specification and its operationalization for the triple graph grammar (TGG) specification technique as an important representative for describing bidirectional model transformations in a relational way. First, we present a formal way to specify attributes in TGG rules in a purely declarative (relational) way. Then, we give an overview of characteristic barriers that bidirectional model transformation tool developers are confronted with when operationalizing relational attribute constraints for different TGG application scenarios. Moreover, we present pragmatic solutions to overcome the operationalization barriers for different TGG application scenarios in our own TGG implementation
EduSymp 2011 - Preface
Get PDFThe Educators’ Symposium focuses on the wide topic of software modeling education ranging from experience reports and case studies to novel pedagogical approaches. Traditionally collocated with the ACM/IEEE International Conference on Model-Driven Engineering Languages and Systems (MODELS), it offers the opportunity for teachers from both academia and industry to present and discuss new ideas and challenges concerning software modeling education. This preface shortly reports on the 7th edition of the Educators’ Symposium held in October 2011 in Wellington, New Zealand
Lens put-put laws: monotonic and mixed
Get PDFMany authors have argued, for good reasons, that in a range of applications the lens put-put law is too strong. On the other hand, the present authors have shown that very well behaved lenses, which do satisfy the put-put law by definition, are algebras for a certain monad, and that this viewpoint admits fruitful generalisations of the lens concept to a variety of base categories. In the algebra approach to lenses, the put-put law corresponds to the associativity axiom, and so is fundamentally important. Thus we have a dilemma. The put-put law seems inappropriate for many applications, but is fundamental to the mathematical development that can support an extended range of applications. In this paper we resolve this dilemma. We outline monotonic put-put laws and introduce a new mixed put-put law that appears to be immune to many of the objections to the classical put-put law, and still supports a very satisfactory mathematical foundation.
Structuring Functional Requirements of Control Systems to Facilitate Refinement-based Formalisation
Get PDFGood requirements structure can greatly facilitate the construction of formal models of systems. This paper describes an approach to requirements structuring for control systems that aims to facilitate refinement-based formalisation. In addition to the well-known monitored and controlled phenomena used to analyse control systems, we also identify commanded phenomenon reflecting the special role that an operator plays in system control. These system phenomena guide the structure of the requirements analysis and documentation as well as the structure of the formal models.We model systems using the Event-B formalism, making use of refinement to support layering of requirements. The structuring provided by the system phenomena and by the refinement layers supports clear traceability and validation between requirements and formal models. As a worked example, we structured the requirements of an automotive lane departure warning system using this approach. We found missing requirements through this process and we evolved the requirement document through domain experts’ feedback and formal modelling
First International Workshop on Bidirectional Transformations (BX 2012): Preface
Get PDFBidirectional transformations (bx) are a mechanism for maintaining the consistency of two (or perhaps more) related sources of information. Such sources can be databases, software models, documents, or their abstract models like graphs or trees. BX are an emerging topic in a wide range of research areas with prominent presence at top conferences in different fields. The methodologies used for bx range from classical program transformation to graph transformation techniques, from ad-hoc techniques for data synchronization to the development of domain-specific languages and their integration. The First International Workshop on Bidirectional Transformations (BX 2012) established a dedicated venue for bx in all relevant areas. It was initiated by the participants of the Dagstuhl Seminar "Bidirectional Transformations" (bx) in Germany 2011, which continued the GRACE International Meeting on Bidirectional Transformations held in Japan 2008.The workshop BX 2012 took place at the Tallinn University of Technology,Estonia on the 25th of March 2012, as a satellite event of ETAPS 2012, the European Joint Conferences on Theory and Practice of Software
Conditions in Reactive Systems and in Graph Rewriting
Get PDFWe introduce conditional reactive systems, by enriching the reactive systems of Leifer and Milner with application conditions. Furthermore we compare tothe situation in graph rewriting where application conditions play a major role
Positioning Verfification in the Context of Software/System Certification
Get PDFFormal verification applied to software has been seen as an important focus in research for determining the acceptability of that software for use. However, in examining the requirements for determining the safety of a software intensive system for use in critical situations, it is quite clear that verification plays a role,but not necessarily a central role. It is entirely possible that a piece of software satisfies its specification, but is unsafe to use. (The first and foremost reason for this is that the program satisfies an unsafe specification.) In this paper we will address the nature of certification in the context of critical systems, decomposing it,by means of a new philosophical framework, into four aspects: evidence, confidence, determination and certification. Our point of view is that establishing the safety (in a very general sense) of a system is a confidence building exercise much in the same vein as the scientific method; our framework serves as a setting in which we can properly understand and develop such an exercise. We will then place formal verification and assurance cases in this setting, discussing their roles and limitations.Keywords: Software certification, System certification, Formal specification, Verification,Critical systems, Safety, Assurance cases, Safety case
Layout Improvement in Diagram Editors by Automatic Ad-hoc Layout
Get PDFLayout, in the context of diagram editors, is the positioning of diagram components on the screen. Editor users enjoy automatic layout, but they usually like to control the layout at runtime, too. Our pattern-based layout approach allows for automatic and user-controlled layout at the same time: The diagram editor may automatically apply layout patterns to diagram parts based on syntactic rules provided by the editor developer, but editor users may also select diagram parts and then apply layout patterns to them. For instance, user-selected components may be aligned horizontally and remain aligned even after diagram modifications.This paper describes continued work on pattern-based layout. We present automatic ad-hoc layout which combines automatic and user-controlled layout in a new way. While automatic layout is syntax-based and must be specified by the editor developer in advance, automatic ad-hoc layout is solely based on the current diagram layout. Whenever the layout engine detects a situation where a pattern may be applied with no or only small diagram changes, this layout pattern is automatically applied. For instance, if a set of components is almost horizontally aligned on the screen, the horizontal alignment pattern is automatically applied to these components. Such an editor behavior is known from so-called snap lines in commercial diagram editors. Automatic ad-hoc layout generalizes on these manually programmed layout solutions and offers many additional layout features.This paper describes the concept of automatic ad-hoc layout as well as its integration into a diagram editor framework and discusses issues of this new layout approach
Visual Contracts as Test Oracle in AGG 2.0
Get PDFA test oracle predicts expected outcomes for a set of test cases, often based on a formal, executable specification. Visual contracts are graph transformation rules describing pre- and post-conditions of a service’s operations. To obtain an oracle based on visual contracts, we use the Attributed Graph Grammar System (AGG) to execute the rules, creating a simulation of the behaviour expected of the system under test.The paper discusses the basic idea, illustrates it by an example, describes the challenges and solutions of its implementation and draws conclusions for the use of graph transformation and AGG in test oracles
Rooted Graph Programs
Get PDFWe present an approach for programming with graph transformation rules in which programs can be as efficient as programs in imperative languages. The basic idea is to equip rules and host graphs with distinguished nodes, so-called roots, and to match roots in rules with roots in host graphs. This enables graph transformation rules to be matched in constant time, provided that host graphs have a bounded node degree (which in practice is often the case). Hence, for example, programs with a linear bound on the number of rule applications run in truly linear time. We demonstrate the feasibility of this approach with a case study in graph colouring