Electronic Communications of the EASST (European Association of Software Science and Technology)
Not a member yet
887 research outputs found
Sort by
Augmenting DSVL Meta-Tools with Pattern Specification, Instantiation and Reuse
Get PDFThis paper describes an approach for using patterns in domain-specific visual language (DSVL) meta-tools. Our approach facilitates DSVL development via high level design-for-reuse and design-by-reuse pattern modelling tools. It provides a simple visual pattern modelling language that is used in parallel with DSVL meta-model specifications for modelling and reusing DSVL structural and behavioural design patterns. It also provides tool support for instantiating and visualising structural patterns, as well as executing behavioural patterns on DSVL model instances
Automated Model Synchronization: A Case Study on UML with Maude
Get PDFDesign specifications of software-intensive systems involve models that have been defined with different modelling languages for different purposes. Hence, a specification can be seen as the description of a system from multiple viewpoints, each providing domain-specific constructs for modelling the system in a more precise way. Such heterogeneity of models can jeopardize the consistency of the specification, because updates in one viewpoint may cause unpredictable design errors in other viewpoints, which can then be transferred to the implementation. OMG’s Meta-Object Facility enhances the automation of the model consistency management by providing a uniform format for different modelling languages. In this paper, we illustrate a technique, based on rewriting logic and on strategies for finding inconsistencies in MOF-based heterogeneous specifications and for resolving them in an automated way
Treewidth, Pathwidth and Cospan Decompositions
Get PDFWe will revisit the categorical notion of cospan decompositions of graphs and compare it to the well-known notions of path decomposition and tree decomposition from graph theory. More specifically, we will define several types of cospan decompositions with appropriate width measures and show that these width measures coincide with pathwidth and treewidth. Such graph decompositions of small width are used to efficiently decide graph properties, for instance via graph automata
Verification of Symmetry Detection using PVS
Get PDFOne of the major limitations of model checking is that of state-space
explosion. Symmetry reduction is a method that has been successfully used to alleviate
this problem for models of systems that consist of sets of identical components.
In earlier work, we have introduced a specification language, Promela-Lite, which
captures the essential features of Promela but has a fully defined semantics. We used
hand proofs to show that a static symmetry detection technique developed for this
language is sound, and suitable to be used in a symmetry reduction tool for SPIN.
One of the criticisms often levelled at verification implementations, is that they have
not been proved mechanically to be correct, i.e., no mechanical formal verification
technique has been used to check the soundness of the approach. In this paper, we
address this issue by mechanically verifying the correctness of the symmetry detection
technique. We do this by embedding the syntax and semantics of Promela-Lite
into the theorem prover PVS and using these embeddings to both check the consistency
of syntax/semantics definitions, and interactively prove relevant theoretical
properties
Support for Bidirectional Model-to-Text Transformations
Get PDFIn recent years, model-driven approaches and processes have established themselves as pragmatic and feasible solutions with tangible advantages. Transformations play a central role in any model-driven solution and, as interest in textual modelling grows, providing concepts and tools for supporting a high-level and declarative specification of bidirectional model-to-text transformations becomes a vital area of research. Our paper identifies important areas and scenarios for model-to-text transformations that are not or only partially supported by currently existing solutions. Based on the requirements of a real-world case study, we introduce a new concept that has been inspired by a successful bidirectional model-to-model transformation approach: Triple Graph Grammars
Propagation of Constraints along Model Transformations Based on Triple Graph Grammars
Get PDFModel transformations based on triple graph grammars (TGGs) have been applied in several practical case studies and they convince by their intuitive and descriptive way of specifying bidirectional model transformations. Moreover, fundamental properties have been extensively studied including syntactical correctness, completeness, termination and functional behaviour.
But up to now, it is an open problem how domain specific properties that are valid for a source model can be preserved along model transformations such that the transformed properties are valid for the derived target model. In this paper, we analyse in the framework of TGGs how to propagate constraints from a source model to an integrated and target model such that, whenever the source model satisfies the source constraint also the integrated and target model satisfy the corresponding integrated and target constraint. In our main new results we show under which conditions this is possible. The case study shows how this result is successfully applied for the propagation of security constraints in enterprise modelling between business and IT models
Static Type Checking of Model Transformation Programs
Get PDFModel transformation is seen as a promising approach to automate software development and verification, thus improving quality and reducing production costs significantly. However, errors of transformation programs can propagate into the generated artifacts complicating the detection of errors. The current paper proposes a static type checking approach for early detection of typing errors of partially typed transformation programs. The approach describes type safety as constraint satisfaction problems, and uses a dedicated back-annotation mechanism for error feedback
Static Analysis of Information Release in Interactive Programs
Get PDFIn this paper we present a model for analysing information release (or leakage) in programs written in a simple imperative language. We present the se- mantics of the language, an attacker model, and the notion of an information release policy. Our key contribution is the static analysis technique to compute information release of programs and to verify it against a policy. We demonstrate our approach by analysing information released to an attacker by faulty password checking pro- grams; our example is inspired by a known flaw in versions of OpenSSH distributed with various Unix, Linux, and OpenBSD operating systems
Dependable keyed data entry for interactive systems
Get PDFKeyed data entry is fundamental and ubiquitous, occurring when filling data fields in web forms, entering burglar alarm pass-codes, using calculators, entering drug delivery rates in infusion pumps, making cash withdrawals from cash machines, setting destinations for GPS navigation, to name but a few of its applications. Unfortunately data entry is often implemented poorly.
We introduce divergence, a loss of predictability in a user interface, and show that it is in general unavoidable in data entry, and therefore a systematic approach is called for. This paper presents one such an approach. Many inter-related ideas ``fall into place''---e.g., autocompletion, prompting, automatic color coding---through the approach. The approach contrasts with conventional systems that are generally inconsistent and unhelpful to users, particularly after errors
A visual language for temporal specifications based on Spider diagrams
Get PDFSpider Diagrams are a well-established visual language to specify sets, their relationships, and constraints on their cardinalities. However, they do not support evolution of specifications, where one wants to state that under certain circumstances a specification becomes invalid and a new one must be used, nor transformation of specifications, where one needs operators to manipulate specifications. In this paper, we attack the first problem by developing a new system of timed Spider Diagrams which allow modellers to indicate the temporal range of validity of a specification. The approach is illustrated with examples of policies for library management