nach oben

2017 | Buch

Kapitel lesen Erstes Kapitel lesen

Fundamentals of Software Engineering

7th International Conference, FSEN 2017, Tehran, Iran, April 26–28, 2017, Revised Selected Papers

herausgegeben von: Mehdi Dastani, Prof. Marjan Sirjani

Verlag: Springer International Publishing

Buchreihe : Lecture Notes in Computer Science

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Einloggen, um Zugang zu erhalten

Über dieses Buch

This book constitutes the thoroughly refereed post-conference proceedings of the 7th International Conference on Fundamentals of Software Engineering, FSEN 2017, held in Tehran, Iran, in April 2017.

The 16 full papers presented in this volume were carefully reviewed and selected from 49 submissions. The topics of interest in FSEN span over all aspects of formal methods, especially those related to advancing the application of formal methods in software industry and promoting their integration with practical engineering techniques.

Inhaltsverzeichnis

Frontmatter

Implementing Open Call-by-Value

Abstract

The theory of the call-by-value \(\lambda \)-calculus relies on weak evaluation and closed terms, that are natural hypotheses in the study of programming languages. To model proof assistants, however, strong evaluation and open terms are required. Open call-by-value is the intermediate setting of weak evaluation with open terms, on top of which Grégoire and Leroy designed the abstract machine of Coq. This paper provides a theory of abstract machines for open call-by-value. The literature contains machines that are either simple but inefficient, as they have an exponential overhead, or efficient but heavy, as they rely on a labelling of environments and a technical optimization. We introduce a machine that is simple and efficient: it does not use labels and it implements open call-by-value within a bilinear overhead. Moreover, we provide a new fine understanding of how different optimizations impact on the complexity of the overhead.

Beniamino Accattoli, Giulio Guerrieri

Debugging of Concurrent Systems Using Counterexample Analysis

Abstract

Model checking is an established technique for automatically verifying that a model satisfies a given temporal property. When the model violates the property, the model checker returns a counterexample, which is a sequence of actions leading to a state where the property is not satisfied. Understanding this counterexample for debugging the specification is a complicated task for several reasons: (i) the counterexample can contain hundreds of actions, (ii) the debugging task is mostly achieved manually, and (iii) the counterexample does not give any clue on the state of the system (e.g., parallelism or data expressions) when the error occurs. This paper presents a new approach that improves the usability of model checking by simplifying the comprehension of counterexamples. Our solution aims at keeping only actions in counterexamples that are relevant for debugging purposes. To do so, we first extract in the model all the counterexamples. Second, we define an analysis algorithm that identifies actions that make the behaviour skip from incorrect to correct behaviours, making these actions relevant from a debugging perspective. Our approach is fully automated by a tool that we implemented and applied on real-world case studies from various application areas for evaluation purposes.

Gianluca Barbon, Vincent Leroy, Gwen Salaün

Bisimilarity of Open Terms in Stream GSOS

Abstract

Stream GSOS is a specification format for operations and calculi on infinite sequences. The notion of bisimilarity provides a canonical proof technique for equivalence of closed terms in such specifications. In this paper, we focus on open terms, which may contain variables, and which are equivalent whenever they denote the same stream for every possible instantiation of the variables. Our main contribution is to capture equivalence of open terms as bisimilarity on certain Mealy machines, providing a concrete proof technique. Moreover, we introduce an enhancement of this technique, called bisimulation up-to substitutions, and show how to combine it with other up-to techniques to obtain a powerful method for proving equivalence of open terms.

Filippo Bonchi, Matias David Lee, Jurriaan Rot

Composing Families of Timed Automata

Abstract

Featured Timed Automata (FTA) is a formalism that enables the verification of an entire Software Product Line (SPL), by capturing its behavior in a single model instead of product-by-product. However, it disregards compositional aspects inherent to SPL development. This paper introduces Interface FTA (IFTA), which extends FTA with variable interfaces that restrict the way automata can be composed, and with support for transitions with atomic multiple actions, simplifying the design. To support modular composition, a set of Reo connectors are modelled as IFTA. This separation of concerns increases reusability of functionality across products, and simplifies modelling, maintainability, and extension of SPLs. We show how IFTA can be easily translated into FTA and into networks of Timed Automata supported by UPPAAL. We illustrate this with a case study from the electronic government domain.

Guillermina Cledou, José Proença, Luis Soares Barbosa

A Formal Model for Multi SPLs

Abstract

A Software Product Line (SPL) is a family of similar programs generated from a common artifact base. A Multi SPL (MPL) is a set of interdependent SPLs that are typically managed and developed in a decentralized fashion. Delta-Oriented Programming (DOP) is a flexible and modular approach to implement SPLs. This paper presents new concepts that extend DOP to support the implementation of MPLs. These extensions aim to accommodate compositional analyses. They are presented by means of a core calculus for delta-oriented MPLs of Java programs. Suitability for MPL compositional analyses is demonstrated by compositional reuse of existing SPL analysis techniques.

Ferruccio Damiani, Michael Lienhardt, Luca Paolini

Translating Active Objects into Colored Petri Nets for Communication Analysis

Abstract

Actor-based languages attract attention for their ability to scale to highly parallel architectures. Active objects combine the asynchronous communication of actors with object-oriented programming by means of asynchronous method calls and synchronization on futures. However, the combination of asynchronous calls and synchronization introduces communication cycles which lead to a form of communication deadlock. This paper addresses such communication deadlocks for ABS, a formally defined active object language which additionally supports cooperative scheduling to express complex distributed control flow, using first-class futures and explicit process release points. Our approach is based on a translation of the semantics of ABS into colored Petri nets, such that a particular program corresponds to a marking of this net. We prove the soundness of this translation and demonstrate by example how the implementation of this net can be used to analyze ABS programs with respect to communication deadlock.

Anastasia Gkolfi, Crystal Chang Din, Einar Broch Johnsen, Martin Steffen, Ingrid Chieh Yu

Synthesizing Parameterized Self-stabilizing Rings with Constant-Space Processes

Abstract

This paper investigates the problem of synthesizing parameterized rings that are “self-stabilizing by construction”. While it is known that the verification of self-stabilization for parameterized unidirectional rings is undecidable, we present a counterintuitive result that synthesizing such systems is decidable! This is surprising because it is known that, in general, the synthesis of distributed systems is harder than their verification. We also show that synthesizing self-stabilizing bidirectional rings is an undecidable problem. To prove the decidability of synthesis for unidirectional rings, we propose a sound and complete algorithm that performs the synthesis in the local state space of processes. We also generate strongly stabilizing rings where no fairness assumption is made. This is particularly noteworthy because most existing verification and synthesis methods for parameterized systems assume a fair scheduler.

Alex P. Klinkhamer, Ali Ebnenasir

Flexible Transactional Coordination in the Peer Model

Abstract

The Peer Model is a model for the specification of coordination aspects found in concurrent and distributed systems. It provides modeling constructs for flows, time, remoting and exception handling. The main concepts of the ground model are peers, wirings, containers, entries and services. Its intent is to introduce specific modeling abstractions of concurrency and distribution to make designs more readable and suitable for larger problems. However, there still exist coordination aspects that are not straight forward to model with it. In this paper, therefore the Peer Model is extended by modeling constructs for nested, distributed transactions based on the Flex transaction model. This approach eases the advanced control of structured and distributed coordination scenarios that have to cope with complex, dependent and concurrent flows. The evaluation introduces a coordination challenge that requires adaptive and transactional distribution of resources, dependencies between concurrent activities, error handling and compensation. It demonstrates the improvements that can be achieved with the new modeling concepts.

Eva Kühn

Using Swarm Intelligence to Generate Test Data for Covering Prime Paths

Abstract

Search-based test data generation methods mostly consider the branch coverage criterion. To the best of our knowledge, only two works exist which propose a fitness function that can support the prime path coverage criterion, while this criterion subsumes the branch coverage criterion. These works are based on the Genetic Algorithm (GA) while scalability of the evolutionary algorithms like GA is questionable. Since there is a general agreement that evolutionary algorithms are inferior to swarm intelligence algorithms, we propose a new approach based on swarm intelligence for covering prime paths. We utilize two prominent swarm intelligence algorithms, i.e., ACO and PSO, along with a new normalized fitness function to provide a better approach for covering prime paths. To make ACO applicable for the test data generation problem, we provide a customization of this algorithm. The experimental results show that PSO and the proposed customization of ACO are both more efficient and more effective than GA when generating test data to cover prime paths. Also, the customized ACO, in comparison to PSO, has better effectiveness while has a worse efficiency.

Atieh Monemi Bidgoli, Hassan Haghighi, Tahere Zohdi Nasab, Hamideh Sabouri

LittleDarwin: A Feature-Rich and Extensible Mutation Testing Framework for Large and Complex Java Systems

Abstract

Mutation testing is a well-studied method for increasing the quality of a test suite. We designed LittleDarwin as a mutation testing framework able to cope with large and complex Java software systems, while still being easily extensible with new experimental components. LittleDarwin addresses two existing problems in the domain of mutation testing: having a tool able to work within an industrial setting, and yet, be open to extension for cutting edge techniques provided by academia. LittleDarwin already offers higher-order mutation, null type mutants, mutant sampling, manual mutation, and mutant subsumption analysis. There is no tool today available with all these features that is able to work with typical industrial software systems.

Ali Parsai, Alessandro Murgia, Serge Demeyer

TCE+: An Extension of the TCE Method for Detecting Equivalent Mutants in Java Programs

Abstract

While mutation testing is considered to be an effective technique in software testing, there are some impediments to its widespread use in industrial projects. One of these challenges is the equivalent mutant problem, and a line of research is dedicated to proposing new methods for addressing this problem. Trivial Compiler Equivalence (TCE) method is recently introduced as a simple technique that actually relies only on the optimizations made by the compiler. It is shown by empirical studies that employing TCE with the gcc compiler results in a fast and effective technique for detecting equivalent mutants in C programs. However, considering the fact that the Java compilers generally do not perform noticeable optimizations, the question is how effectively does TCE perform on Java programs? In this paper, experimental evaluations are discussed which demonstrate that using TCE technique with javac compiler results in very poor performance. As a result, this paper proposes to use the Java obfuscators as the complementary component, because of the optimizations they make. The experimental evaluations confirm that using TCE with the ProGuard obfuscation tool provides an effective and efficient method for detecting equivalent mutants in Java programs.

Mahdi Houshmand, Samad Paydar

Quality-Aware Reactive Programming for the Internet of Things

Abstract

The reactive paradigm recently became very popular in user-interface development: updates — such as the ones from the mouse, keyboard, or from the network — can trigger a chain of computations organised in a dependency graph, letting the underlying engine control the scheduling of these computations. In the context of the Internet of Things (IoT), typical applications deploy components in distributed nodes and link their interfaces, employing a publish-subscribe architecture. The paradigm for Distributed Reactive Programming marries these two concepts, treating each distributed component as a reactive computation. However, existing approaches either require expensive synchronisation mechanisms or they do not support pipelining, i.e., allowing multiple “waves” of updates to be executed in parallel.

We propose Quarp (Quality-Aware Reactive Programming), a scalable and light-weight mechanism aimed at the IoT to orchestrate components triggered by updates of data-producing components or of aggregating components. This mechanism appends meta-information to messages between components capturing the context of the data, used to dynamically monitor and guarantee useful properties of the dynamic applications. These include the so-called glitch freedom, time synchronisation, and geographical proximity. We formalise Quarp using a simple operational semantics, provide concrete examples of useful instances of contexts, and situate our approach in the realm of distributed reactive programming.

José Proença, Carlos Baquero

Purpose-Based Policy Enforcement in Actor-Based Systems

Abstract

Preserving data privacy is a challenging issue in distributed systems as private data may be propagated as part of the messages transmitted among system components. We study the problem of preserving data privacy on actor model as a well known reference model for distributed asynchronous systems. Our approach to prevent private data disclosure is to enforce purpose-based privacy policies which control the access and usage of private data. We propose a method to specify purposes based on workflows modeled by Petri nets in which transitions correspond to message communications. We first use model checking to verify whether the actor model behaves conforming to the purpose model. Then, the satisfaction of the policies are checked using data dependence analysis. We also provide a method to evaluate the effectiveness of policies through checking of private data disclosure in the presence of privacy policies. Since these checks are performed statically at design time, no runtime overhead is imposed on the system.

Shahrzad Riahi, Ramtin Khosravi, Fatemeh Ghassemi

Automatic Transition System Model Identification for Network Applications from Packet Traces

Abstract

A wide range of network management tasks such as balancing bandwidth usage, firewalling, anomaly detection and differentiating traffic pricing, depend on accurate traffic classification. Due to the diversity and variability of network applications, port-based and statistical signature detection approaches become inefficient and hence, behavioral classification approaches have been considered recently. However, so far, there is no automated general method to obtain the behavioral models of applications. In this research, we propose an automatic procedure to infer a transition system model from generated traffic of an application. Our approach is based on passive automata learning theory and evidence driven state merging technique using the rules of the network domain. We consider the behavior of well-known network protocols to generate the model which includes unobserved behaviors and excludes invalid ones as much as possible. To this aim, we present a new equivalence relation regarding the given protocol behaviors to induce proper state merging conditions. This idea has led the time complexity order of the algorithm to be linear rather than exponential. Finally, we apply the model of some real applications to evaluate the precision and execution time of our approach.

Zeynab Sabahi-Kaviani, Fatemeh Ghassemi, Fateme Bajelan

Gray-Box Conformance Testing for Symbolic Reactive State Machines

Abstract

Model-based testing (MBT) is typically a black-box testing technique. Therefore, generated test suites may leave some untested gaps in a given implementation under test (IUT). We propose an approach to use the structural and behavioural information exploited from the implementation domain to generate effective and efficient test suites. Our approach considers both specification models and implementation models, and generates an enriched test model which is used to automatically generate test suites. We show that the proposed approach is sound and exhaustive and cover both the specification and the implementation. We examine the applicability and the effectiveness of our approach by applying it to a well-known example from the railway domain.

Masoumeh Taromirad, Mohammad Reza Mousavi

Model Checking of Concurrent Software Systems via Heuristic-Guided SAT Solving

Abstract

An established approach to software verification is SAT-based bounded model checking where a state space model is encoded as a Boolean formula and the exploration is performed via SAT solving. Most existing approaches in SAT-based model checking rely on general-purpose solvers that do not exploit the structural features of the encoding. Aiming at a significantly better runtime performance in such settings, we show in this paper that SAT algorithms can be specifically tailored w.r.t. the structure of the Boolean encoding of the model checking problem to be solved. We define a state space encoding of concurrent software systems that preserves control flow information. This allows to modify the solver such that the number of SAT decision levels can be significantly reduced by assigning a set of atoms at each level. Such set assignment always characterises a location in the control flow of the encoded system. Moreover, we introduce heuristics that guide the SAT search into directions where a violation of the property of interest may be most likely detected. The heuristic approach enables to quickly discover errors while keeping the actually explored part of the state space small.

Nils Timm, Stefan Gruner, Prince Sibanda

Backmatter

Titel: Fundamentals of Software Engineering
herausgegeben von: Mehdi Dastani
Prof. Marjan Sirjani
Verlag: Springer International Publishing
Electronic ISBN: 978-3-319-68972-2
Print ISBN: 978-3-319-68971-5
DOI: https://doi.org/10.1007/978-3-319-68972-2