Vehicle platooning is a promising technology to save the road capacity and also fuel consumption by reducing the distance between the vehicles in the platoon. The closer the cars are to each other, the closer we are to the goals. But, this will increase the need for safety verification. In this paper we use formal methods to verify safety distance in a platoon. To do so, we present a formal actor-based model for a vehicle platoon which incorporates vehicle dynamics and communication protocol. Also, we present a method to do the analysis based on model checking that applies mathematical analysis to reduce the state space. The method uses an upper bound and a lower bound value as network delay, and verifies if a specified vehicle in a platoon has enough distance to the leader during its traveling.

In the new generation of message-based systems such as network-based smart systems, distributed components collaborate via asynchronous message passing. In some cases, particular ordering among the messages may lead to violation of the desired properties such as data confidentiality. Due to the absence of a global clock and usage of off-the-shelf components, there is no control over the order of messages at design time. To make such systems safe, we propose a choreography-based runtime enforcement algorithm that given an automata-based specification of unwanted message sequences, prevents certain messages to be sent, and assures that the unwanted sequences are not formed. Our algorithm is fully decentralized in the sense that each component is equipped with a monitor, as opposed to having a centralized monitor. As there is no global clock in message-based systems, the order of messages cannot be determined exactly. In this way, the monitors behave conservatively in the sense that they prevent a message from being sent, even when the sequence may not be formed. We aim to minimize conservative prevention in our algorithm when the message sequence has not been formed. The efficiency and scalability of our algorithm are evaluated in terms of the communication overhead and the blocking duration through simulation.

Dynamic creating of objects and processes as one of the widely used techniques for developing models does not support by the majority of model checking tools. In addition, although there exist few model checking tools which support dynamic creation of model elements, e.g. Spin, they do not provide a property language for presenting the behavioral specifications of dynamically created elements. In this paper, we address this shortage and provide proper support for the model checking of object-based models which contain dynamic object creation. To this aim, we propose LeeTL, a new temporal logic that supports quantifications over model objects. Using LeeTL, it is also possible to traverse objects to access the variables of the objects for defining property formulas. We propose an algorithm for transforming LeeTL formulas to Büchi automata to be able to use the existing model checking tools which support Büchi automata.

Abstract Wireless ad hoc networks, in particular mobile ad hoc networks (MANETs), are growing very fast as they make communication easier and more available. However, their protocols tend to be difficult to design due to topology dependent behavior of wireless communication, and their distributed and adaptive operations to topology dynamism. Therefore, it is desirable to have them modeled and verified using formal methods. In this paper, we present an actor-based modeling language with the aim to model MANETs. We address main challenges of modeling wireless ad hoc networks such as local broadcast, underlying topology, and its changes, and discuss how they can be efficiently modeled at the semantic level to make their verification amenable. The new framework abstracts the data link layer services by providing asynchronous (local) broadcast and unicast communication, while message delivery is in order and is guaranteed for connected receivers. We illustrate the applicability of our framework through two routing protocols, namely flooding and AODVv2-11, and show how efficiently their state spaces can be reduced by the proposed techniques. Furthermore, we demonstrate a loop formation scenario in AODV, found by our analysis tool.

Software Product Line Engineering is an approach to management of diversity in software families. Although several SPLE approaches exist in the domains of industrial software applications, product lines of data-intensive software systems have gained less attention. We use an incremental, delta-oriented technique to handle variability by specifying changes to be made to a core data model to define the data schemas of the products. We present a new merge-prune operator based on the superimposition of models as well as the structural well-formedness rules specified formally in Alloy. Our method provides a modular way to handle variability in data intensive systems. It is scalable with respect to the number of variation points in the system in contrast to the traditional annotative approaches for variability modeling. We have investigated the applicability of our approach by using it in a real-world case study.

Multi product lines (MPLs) are systems consisting of collections of interdependent software product lines (SPLs). The dependencies and interactions among the SPLs cause new challenges in variability management. In the case of a large-scale information system MPL, important issues are raised regarding integration of the databases of the individual SPLs comprising the main system. The aim of this paper is to introduce a method to manage the variability in the data model of such systems. To this end, we first address the problem of developing a universal feature model of the MPL, obtained from integrating the feature models of the individual SPLs, incorporating the data interdependencies among the features. Further, we develop the data model of the MPL using a delta-oriented technique, based on the universal feature model. Our method addresses the problem of possible conflicts among the data model elements of different SPLs and proposes techniques to resolve the conflicts based on data model refinements.

Nowadays, Software Product Lines (SPLs) are being used in a variety of domains including safety-critical systems for which verification of the systems is a matter of concern. Formal modeling and verification of SPLs has been majorly investigated recently. Due to the potential large number of the products in a SPL, individual verification of all products could be costly or even impractical. Hence, there is a need for verification methods that can verify the whole family's behavior at once. In this paper, we focus on the probabilistic model checking of software product lines in which the behavior of individual products can be described in terms of Markov decision processes. We introduce a mathematical model, Markov Decision Process Family (MDPF), to compactly represent the behavior of the whole family. We also provide a model checking algorithm in order to verify MDPFs against properties expressed in probabilistic computational tree logic.

Managing variability in a software family is crucial to software product line engineering. The existing variability management techniques, however do not particularly address database design in the context of information systems poduct lines. This paper presents a practical approach to handle variability in database design for families of software. We use the technique of Delta-Oriented Programming when a product is constructed by adding a number of delta modules to a core module incrementally, based on the features selected in the product configuration. We use SQL Data Definition Language to model core and delta modules. We present rules for consistency checking of the delta scripts based on the database consistency constraints to generate a valid consistent database schema for the product. Also we analyze the cases in which a conflict arises based on inconsistencies between delta modules. The fact that DDL is widely known to software developers, along with modularity and scalability of the proposed method makes it suitable to be used in industrial real world applications.

A software product line describes explicitly the commonalities of and differences between different products in a family of (software) systems. A formalization of these commonalities and differences amounts to reduced development, analysis and maintenance costs in the practice of software engineering. An important feature common to next-generation real-time software systems is the need of application-level control over scheduling for optimized utilization of resources provided by for example many-core and cloud infrastructures. In this paper, we introduce a formal model of real-time software product lines which supports variability in scheduling policies and rigorous and efficient techniques for modular schedulability analysis.

As the development in a software project goes on, the structure of the implemented code diverges from the intended architecture. To prevent this, architecture conformance methods are used to check if the source code complies with the architecture. In the development of today's enterprise applications, general-purpose programming languages are used along with a number of domain specific languages. So, there is a need for a conformance checking method to support multi-language source artifacts. We present a model-based approach for checking cross-language architecture conformance rules. Our method is extensible, in the sense that it is independent of the specific set of languages used in the project.

Modeling variability is a key aspect of variability management in software product families. Product line architecture (PLA) is one of the major assets of a product line, from which individual product architectures are derived. Consequently, modeling variability in architecture becomes an issue worthy of consideration. In this paper, we propose a variability modeling method which is specifically devised for the component and connector (C&C) view of architecture. We use UML 2 as the architecture modeling language. Modeling solutions are proposed and classified based on the type of variable element and the techniques used to realize variability. We have also studied the ways to avoid cluttering the view when including variability. An example case is utilized to clarify different aspects of our proposed method.