Abstract Interaction models describe distributed systems as algebraic terms, with gates marking interaction points between local views. Composing local models into a coherent global one requires aligning these gates while respecting the algebraic laws of interaction operators. This is achieved via anti-unification techniques. We specialize anti-unification (or generalization) via a special constant-preserving variant, which preserves designated constants while generalizing the remaining structure. We develop a dedicated rule-based procedure, for computing these generalizations, prove its termination, soundness, and completeness, extend it modulo equational theories, and integrate it into a standard anti-unification framework. A prototype tool demonstrates the approach’s ability to recompose global interactions from partial views.

Abstract Process mining is concerned with deriving formal models capable of reproducing the behaviour of a given organisational process by analysing observed executions collected in an event log . The elements of an event log are finite sequences (called also traces or words ) of actions. Many effective algorithms have been introduced which issue a control flow model (commonly in Petri net form) aimed at reproducing, as precisely as possible, the language of the considered event log. However, given that identical executions can be observed several times, traces of an event log are associated with a frequency and, hence, an event log inherently yields also a stochastic language . By exploiting the trace frequencies contained in the event log, the stochastic extension of process mining, therefore, consists in deriving stochastic (Petri net) models capable of reproducing the likelihood of the observed executions. In this paper, we introduce a novel stochastic process mining approach. Starting from a non-stochastic Petri net model mined through classical mining algorithms, we employ optimization to identify optimal weights for the transitions of the mined net so that the stochastic language issued by the stochastic interpretation of the mined net closely resembles that of the event log. The optimization is either based on the maximum likelihood principle or on the earth moving distance and we study in detail the characteristics of the associated objective function in both cases. It turns out that the objective function in case of using the maximum likelihood approach lends itself better to optimization. Experiments on some popular real system logs show an improved accuracy with respect to alternative approaches.

This paper presents an approach leveraging symbolic execution techniques to generate test cases from models mixing data and time. Our methodology focuses on symbolic paths, satisfying a trace-determinism property, which allows testing behaviors in the presence of uninitialized state variables. We construct tree-like test cases around these test purposes, with verdicts on their leaves, meticulously crafting verdict conditions from symbolic execution path conditions encoding temporal data-dependent constraints. Our test case generation is implemented within the symbolic execution platform Diversity. Through experiments, we provide metrics and quantify some aspects of the generated test cases, including the reachability of verdicts within observation time frames specified by the tester.

Abstract Labeled graphs are particularly well adapted to represent objects in the context of topology-based geometric modeling. Thus, graph transformation theory is used to implement modeling operations and check their consistency. This article defines a class of graph transformation rules dedicated to embedding computations. Objects are here defined as a particular subclass of labeled graphs in which arc labels encode their topological structure (i.e., cell subdivision: vertex, edge, face) and node labels encode their embedding (i.e., relevant data: vertex positions, face colors, volume density). Object consistency is defined by labeling constraints which must be preserved by modeling operations that modify topology and/or embedding. Dedicated graph transformation variables allow us to access the existing embedding from the underlying topological structure (e.g., collecting all the points of a face) in order to compute the new embedding using user-provided functions (e.g., compute the barycenter of several points). To ensure the safety of the defined operations, we provide syntactic conditions on rules that preserve the object consistency constraints.

Interaction languages such as MSC are often associated with formal semantics by means of translations into distinct behavioral formalisms such as automatas or Petri nets. In contrast to translational approaches we propose an operational approach. Its principle is to identify which elementary communication actions can be immediately executed, and then to compute, for every such action, a new interaction representing the possible continuations to its execution. We also define an algorithm for checking the validity of execution traces (i.e. whether or not they belong to an interaction’s semantics). Algorithms for semantic computation and trace validity are analyzed by means of experiments.

Modular deductive verification is a powerful technique capable to show that each function in a program satisfies its contract. However, function contracts do not provide a global view of which high-level (e.g. security-related) properties of a whole software module are actually established, making it very difficult to assess them. To address this issue, this paper proposes a new specification mechanism, called meta-properties. A meta-property can be seen as an enhanced global invariant specified for a set of functions, and capable to express predicates on values of variables, as well as memory related conditions (such as separation) and read or write access constraints. We also propose an automatic transformation technique translating meta-properties into usual contracts and assertions, that can be proved by traditional deductive verification tools. This technique has been implemented as a Frama-C plugin called MetAcsl and successfully applied to specify and prove safety- and security-related meta-properties in two illustrative case studies.

Abstract Program slicing can be used to reduce a given initial program to a smaller one (a slice ) that preserves the behavior of the initial program with respect to a chosen criterion. Verification and validation (V&V) of software can become easier on slices, but require particular care in the presence of errors or non-termination in order to avoid unsound results or a poor level of code reduction in slices with respect to the initial program. This article proposes a theoretical foundation for conducting V&V activities on a slice instead of the initial program. We introduce the notion of relaxed slicing that is still capable of producing small slices, even in the presence of errors or non-termination, and establish an appropriate soundness property. It allows us to give a precise interpretation of verification results (absence or presence of errors) obtained for a slice in terms of the initial program. The implementation of these results in the Coq proof assistant is presented and some of its difficult points are discussed.

The progressive integration of software-based components into the electricity grid has given raise to what is known as Smart Grids. As long as Smart Grids gain on connectivity and automation, new concerns on their safety and security have arisen. It is agreed that non-negligible risks and enlarged impact due to misbehaviors and intrusions exist. Following a model driven paradigm, a method is proposed to reinforce the security of these complex widely distributed systems. The method guides system re-engineering and is based upon timed models. It encompasses reverse engineering, symbolic, and testing techniques to model, analyze, and deploy attack testing. In early stages of the method, a reference timed model to support security analyses is designed via reverse engineering and symbolic execution. During latter stages, the nominal models are enriched so as to specify attack scenarios which are symbolically executed to prove the ability of the system to detect attacker intrusions. In final stages, the attack scenarios are used to specify test cases which are later deployed to test the system. The method and main outcomes are presented relying upon a Smart Grid subsystem analyzed in the scope of a joint academy-industry project.

Summary In the context of testing from algebraic specifications, test cases are ground formulas chosen amongst the ground semantic consequences of the specification, according to some possible additional observability conditions. A test set is said to be exhaustive if every programmePpassing all the tests is correct and if for every incorrect programmeP, there exists a test case on whichPfails. Because correctness can be proved by testing on such a test set, it is an appropriate basis for the selection of a test set of practical size. The largest candidate test set is the set of observable consequences of the specification. However, depending on the nature of specifications and programmes, this set is not necessarily exhaustive. In this paper, we study conditions to ensure the exhaustiveness property of this set for several algebraic formalisms (equational, conditional positive, quantifier free and with quantifiers) and several test hypotheses. Copyright © 2016 John Wiley & Sons, Ltd.

Remotely-communicating software-based systems are tightly present in modern industrial society and securing their complex architecture is recognized as crucial. In particular, the perspectives to reinforce their security by monitoring are promising. However, monitoring schemes still face challenges as the presence of untrusted components seems unavoidable. Specially, since untrusted components may be placed in unsupervised areas, making them ideal targets for attackers. In this work, we propose a framework intended to support designers during systems conception. The approach mainly relies upon Security Watchdogs committed to detect and signal distrustful activity. A model-based framework is introduced to ease attacks descriptions upon scenarios in the form of UML sequence diagrams. The scenarios endowed with predefined attack patterns are analyzed using models transformations and symbolic techniques. By doing so, the effectiveness of watchdogs is confronted against attacks and the results can be used to reinforce the overall security of the system. The applicability of the proposed method is also shown by means of a Smart Grid case study.

An orchestrator in a Web Service system is a locally deployed piece of software used both to allow users to interact with the system and to communicate with remote components (Web Services) in order to fulfill a goal. We propose a symbolic model based approach to test orchestrators in the context of the systems they pilot. Our approach only takes as input a model of the orchestrator and no models of the Web Services. Besides, the testing architecture is a parameter: communications between Web Services and the orchestrator can be either simulated, or hidden or observable. When they are simulated, the orchestrator is tested in isolation and our approach comes to already defined classical model-based unit testing approaches. When the System Under Test is connected with Web Services (that is, in actual usage) it is no longer fully controlled by the tester, but tested in context In that case two situations may occur: either communications with Web Services are observable or they are hidden. Our approach copes with those cases. We give theorems relating our notion of conformance in context with regard to classical conformance of components in isolation. We present a test case generation algorithm based on symbolic execution techniques: it takes into account the status (controllable, hidden, or observable) of communication channels between the orchestrator and Web Services. The algorithm has been implemented and is illustrated on a small case study.

In this article, we present a rule-based language dedicated to topological operations and based on graph transformations. Generalized maps are described as a particular class of graphs determined by consistency constraints. Hence, topological operations over generalized maps can be specified using graph transformations. The rules we define are provided with syntactic criteria which ensure that graphs computed by applying rules on generalized maps are also generalized maps. We have developed a static analyzer of transformation rules which checks the syntactic criteria in order to ensure the preservation of generalized map consistency constraints. Based on this static analyzer, we have designed a rule-based prototype of a kernel of a topology-based modeler that is generic in dimension. Since adding a new topological operation can be reduced to write a graph transformation rule, we directly obtain an extensible prototype where handled topological objects satisfy built-in consistency. Moreover, first benchmarks show that our prototype is reasonably efficient compared to a reference implementation of 3D generalized maps which use a classical implementation style.

Reactive systems are often described by interconnecting sub-components along architectural connectors defining communication policies. Generally, such global systems may exhibit properties, often called "emergent properties", that cannot be anticipated just from a complete knowledge of components. These emergent properties are twofold: (1) the global system can question properties attached to components; (2) some global properties cannot be inferred only from a complete knowledge of components, but for being inferred, need the knowledge of cooperation mechanisms between components. In practice, properties of the second form combine knowledge inherited from components. Thus, they are often defined in a richer language than the ones associated to each component and the presence of such emergent properties is quite natural. In this paper, we restrict ourselves to reactive systems described by means of transition systems as components and of the usual synchronous product as architectural connector and whose behavior is expressed by logical properties over a modal first-order logic. In this framework, we propose to study complexity of reactive systems through this notion of emergent properties and we will give some conditions to guarantee when a system has not emergent properties of the first form.

A mathematical denotation is proposed for the notion of complex software systems whose behavior is specified by rigorous formalisms. Complex systems are described in a recursive way as an interconnection of subsystems by means of architectural connectors. In order to consider the largest family of specification formalisms and architectural connectors, this denotation is essentially formalism, specification and connector independent. For this, we build our denotation on Goguen's institution theory. We then denote in this abstract framework, complexity by the notion of property emergence.

Structural testing is usually restricted to unit tests and based on some clear definition of source code coverage. In particular, the all-paths criterion, which requires at least one test-case per feasible path of the function under test, is recognised as offering a high level of software reliability. This paper deals with the difficulties of using structural unit testing to test functions which call other functions. To limit the resulting combinatorial explosion in the number of paths, we choose to abstract the called functions by their specification. We incorporate the functional information on the called functions within the structural information on the function under test, given as a control flow graph (CFG). This representation combining functional and structural descriptions may be viewed as an extension of the classic CFG and allows us to characterise test selection criteria ensuring the coverage of the source code of the function under test. Two new criteria will be proposed. The first criterion corresponds to the coverage of all the paths of this new representation, including all the paths arising from the functional description of the called functions. The second criterion covers all the feasible paths of the function under test only. We describe how we automate test-data generation with respect to such grey-box (combinations of black- box and white-box) test selection strategies, and we apply the resulting extension of our PathCrawler tool to examples coded in the C language.

In this paper, we present a temporal logic called /spl Fscr/ whose interpretation is over input output symbolic transition systems (IOSTS). IOSTS extend transition systems to communications and data in order to tackle communications with system environment. /spl Fscr/ is then defined as an extension of temporal logic CTL* (a temporal logic which mixes together the features of linear temporal logic (LTL) and computational temporal logic (CTL)). Three basic properties are established on /spl Fscr/: adequacy and preservation of properties along synchronized product and IOSTS refinement.

We present an institution of feature logics which generalises our earlier approach (2001) and define a refinement theory to deal with the complexity of feature interactions in this generic framework, which is one of the main problems encountered when dealing with feature interaction detection. The study of interactions through implementation techniques is still an open problem. The authors furnish answers to encounter this purpose in a logic-independent framework, using algebraic refinement techniques.

We propose a framework for "probabilistic functional testing."The success of a test data set generated according to our method guarantees a certain level of confidence into the correctness of the system under test, as a function of two parameters.One is an estimate of the reliability, and the other is an estimate of the risk that the vendor takes when (s)he notifies this reliability percentage to the client.These results are based on the theory of "formula testing~' developed in the article.We also present a first prototype of a tool which assists test case generation according to this theory.Lastly, we illustrate our method on a small formal specification.