Electronic Communications of the EASST (European Association of Software Science and Technology)
Not a member yet
887 research outputs found
Sort by
A Pattern Language for the Evolution of Component-based Software Architectures
Get PDFArchitecture-centric software evolution enables change in a system’s structure and behaviour while maintaining a global view of the software to address evolution-centric trade-offs. The existing solutions for architectural maintenance and evolution fall short of exploiting generic and reusable expertise to address recurring evolution problems. We present a pattern language as a collection of interconnected change patterns that enable reuse-driven and consistent evolution of component-based software architectures. Pattern interconnections represent possible relationships among patterns (such as variants or related patterns) in the language. In general, we introduce architecture change mining (pattern language development) as a complementary and integrated phase to facilitate reuse-driven architecture change execution (pattern language application). We evaluate the language applicability to support pattern-driven reuse in architecture evolution of a payment system case study. We also analyse the precision and recall factor as a measure of selecting the most appropriate pattern(s) from the language collection. The pattern language itself continuously evolves with an incremental discovery of new patterns from change logs over tim
Conformance Testing of Cyber-Physical Systems: A Comparative Study
Get PDFFor systematic and automatic testing of cyber-physical systems, in which a set of test cases is generated based on a formal specification, a number of notions of conformance testing have been proposed. In this paper, we review two existing theories of conformance testing for cyber-physical systems and compare them. We point out their fundamental differences, and prove under which assumptions they coincide
Handling Clone Mutations in Simulink Models with VCL
Get PDFLike any other software system, real life Simulink models contain a considerable amount of cloning. These clones are not always identical copies of each other, but actually show a variety of differences from each other despite the overall similarities. Insufficient variability mechanisms provided by the platform make it difficult to create generic structures to represent these clones. Also, complete elimination of clones from the systems may not always be practical, feasible, or cost-effective. In this paper we propose a mechanism for clone management based on Variant Configuration Language (VCL) that provides a powerful variability handling mechanism. In this mechanism, the clones will be managed separate from the models in a non-intrusive way and the original models will not be polluted with extra complexity to manage clone instances. The proposed technique is validated by creating generic solutions for Simulink clones with a variety of differences present between them
From System Requirements to Software Requirements in the Four-Variable Model
Get PDFThe four-variable model of software-controlled embedded systems originally proposed by Parnas and Madey has been used successfully in the development of safety-critical applications in various industries. The model does not explicitly specify the software requirements, but rather bounds them by specifying the system requirements and the input and output hardware interfaces of the system. The software engineers are left with the problem of how to construct software that satisfies the system requirements and hardware interfacing constraints. After formalizing the properties of acceptable system and software implementations using the demonic calculus of relations, we provide (i) a necessary and sufficient condition for the existence of an acceptable software implementation and (ii) a mathematical characterization of the software requirements in terms of their weakest specification
Mean Quantitative Coverability in Stochastic Graph Transformation Systems
Get PDFMany classical problems for Petri nets, in particular reachability and coverability, have obvious counterparts for graph transformation systems. Similarly, many problems for stochastic Petri nets, seen as a model for chemical reaction networks, are special cases of corresponding problems in graph transformation. For example, the evolution of the counts of chemical species in a test tube over time is a typical phenomenon from chemistry, which can faithfully be modelled and analysed using stochastic Petri nets. The corresponding mean quantitative coverability problem for stochastic graph transformation is simple to describe – yet hard to solve. This extended abstract summarises the fundamental ideas and challenges
Towards Model Checking Reconfigurable Petri Nets using Maude
Get PDFThis paper introduces an approach to model checking of reconfigurable Petri nets. The main task is to flatten the two levels of dynamic behavior that reconfigurable nets provide, the firing of transitions on the one hand and the transformation of the nets on the other hand. We show how to translate a reconfigurable net into Maude modules. Maude's LTL model-checker is then used to verify properties of these modules
Analyzing Conflict Freedom for Multi-threaded Programs With Time Annotations
Get PDFAvoiding access conflicts is a major challenge in the design of multi-threaded programs. In the context of real-time systems, the absence of conflicts can be guaranteed by ensuring that no two potentially conflicting accesses are ever scheduled concurrently.In this paper, we analyze programs that carry time annotations specifying the time for executing each statement. We propose a technique for verifying that a multi-threaded program with time annotations is free of access conflicts. In particular, we generate constraints that reflect the possible schedules for executing the program and the required properties. We then invoke an SMT solver in order to verify that no execution gives rise to concurrent conflicting accesses. Otherwise, we obtain a trace that exhibits the access conflict
Using SMT for dealing with nondeterminism in ASM-based runtime verification
Get PDFIn runtime verification, operational models describing the expected system behavior offer some advantages with respect to declarative specifications of properties, especially when designers are more accustomed to them. However, nondeterminism in the specification usually affects performances of those operational methods that explicitly represent all the possible conformant states. In this paper, we tackle the problem of dealing with nondeterminism in an operational runtime verification approach based on the use of Abstract State Machines (ASMs). We propose an SMT-based technique in which ASM computations are symbolically represented and conformance verification is performed by means of satisfability checking. Experiments show that, in most of the cases, the symbolic approach performs better than a technique for ASM-based runtime verification explicitly representing the conformant states
Verifying a Mix Net in CSP
Get PDFA Mix Net is a cryptographic protocol that tries to unlink the correspondence between its inputs and its outputs. In this paper, we formally analyse a Mix Net using the process algebra CSP and its associated model checker FDR. The protocol that we verify removes the reliance on a Web Bulletin Board during the mixing process: rather than communicating via a Web Bulletin Board, the protocol allows the mix servers to communicate directly, exchanging signed messages and maintaining their own records of the messages they have received. Mix Net analyses in the literature are invariably focused on safety properties; important liveness properties, such as deadlock freedom, are wholly neglected. This is an unhappy omission, however, since a Mix Net that produces no results is of little use. Here we verify that the Mix Net is guaranteed to terminate, outputting a provably valid mix agreed upon by a majority of mix servers, under the assumption that a majority of them act according to the protocol
Analyzing Gerrit Code Review Parameters with Bicho
Get PDFCode review is becoming a common practice in large scale software development projects. In the case of free, open source software projects, many of them are selecting Gerrit as the system to support the code review process. Therefore, the analysis of the information produced by Gerrit allows for the detailed tracking of the code review process in those projects. In this paper, we present an approach to retrieve and analyze that information based on extending Bicho, a tool designed to retrieve information from issue tracking systems. The details of the retrieval process, the model used to map code review abstractions to issue tracking abstractions, and the structure of the retrieved information are described in detail. In addition, some results of using this approach in a real world scenario, the OpenStack Gerrit code review system, are presented