Fundamenta Informaticae - Volume 182, issue 1

Authors: Keller, Jörg | Penczek, Wojciech

Article Type: Other

DOI: 10.3233/FI-2021-2063

Citation: Fundamenta Informaticae, vol. 182, no. 1, pp. v-vi, 2021

Authors: Felli, Paolo | de Leoni, Massimiliano | Montali, Marco

Article Type: Research Article

Abstract: Traditionally Business Process Modeling has only focused on the control-flow perspective, thus allowing process designers to specify the constraints on the activities of the process: the order and potential concurrency of their execution, their mutual exclusivity, the possibility of being repeated, etc. However, activities are executed by different resources, manipulate data objects and are constrained by the state of such objects. This requires that the traditional notion of soundness, typically introduced for control-flow-only models, is extended so as to consider data. Intuitively, a (data-aware) process model is sound if (1) it does not contain deadlocks, (2) no more activities are …enabled when the process instance is marked as completed and finally (3) there are no parts of the model that cannot be executed. Although several data-aware notations have been introduced in the literature, not all of these are given a formal semantics. In this paper, we propose a technique for checking the data-aware soundness for a specific class of such integrated models, with a simple syntax and semantics, building on Data Petri Nets (DPNs). These are Petri nets enriched with case variables, where transitions are guarded by formulas that inspect and update such variables, and are of the form variable-operator-variable or variable-operator-constant. Even though DPNs are less expressive than Petri nets where data are carried by tokens, they elegantly capture business processes operating over simple case data, allowing to model complex data-aware decisions. We show that, if a DPN is data-aware sound, the Constraint Graph is a finite-state automaton; however, a finite-state Constraint Graph does not guarantee data-aware soundness, but provides a finite structure through which this property can be checked. Finally, we investigate further properties beyond data-aware soundness, such as the problem of verifying that an actor participating in the business process can unilaterally enforce data-aware soundness by restricting the possible executions of a bounded DPN, assuming this actor to be able to control the firing of some transitions and decide the value of some of the case variables whenever these are updated. Show more

Keywords: Soundness of Process Models, Data Perspective, Data Petri Nets

DOI: 10.3233/FI-2021-2064

Citation: Fundamenta Informaticae, vol. 182, no. 1, pp. 1-29, 2021

Authors: André, Étienne | Coquard, Emmanuel | Fribourg, Laurent | Jerray, Jawher | Lesens, David

Article Type: Research Article

Abstract: The next generation of space systems will have to achieve more and more complex missions. In order to master the development cost and duration of such systems, an alternative to a manual design is to automatically synthesize the main parameters of the system. In this paper, we present an approach for the specific case of the scheduling of the flight control of a space launcher. The approach requires two successive steps: (1) the formalization of the problem to be solved in a parametric formal model and (2) the synthesis of the model parameters with a tool. We first describe the …problem of the scheduling of a launcher flight control, then we show how this problem can be formalized with parametric stopwatch automata; we then present the results computed by the parametric timed model checker IMITATOR . We enhance our model by taking into consideration the time for switching context, and we compare the results to those obtained by other tools classically used in scheduling. Show more

Keywords: scheduling, real-time systems, model checking, parameter synthesis, IMITATOR

DOI: 10.3233/FI-2021-2065

Citation: Fundamenta Informaticae, vol. 182, no. 1, pp. 31-67, 2021

Authors: André, Étienne | Lime, Didier | Ramparison, Mathias | Stoelinga, Mariëlle

Article Type: Research Article

Abstract: Risk assessment of cyber-physical systems, such as power plants, connected devices and IT-infrastructures has always been challenging: safety (i. e., absence of unintentional failures) and security (i. e., no disruptions due to attackers) are conditions that must be guaranteed. One of the traditional tools used to consider these problems is attack trees, a tree-based formalism inspired by fault trees, a well-known formalism used in safety engineering. In this paper we define and implement the translation of attack-fault trees (AFTs) to a new extension of timed automata, called parametric weighted timed automata. This allows us to parameterize constants such as time …and discrete costs in an AFT and then, using the model-checker IMITATOR , to compute the set of parameter values such that a successful attack is possible. Moreover, we add the possibility to define counter-measures. Using the different sets of parameter values computed, different attack and fault scenarios can be deduced depending on the budget, time or computation power of the attacker, providing helpful data to select the most efficient counter-measure. Show more

Keywords: security, attack-fault trees, parametric timed automata, IMITATOR

DOI: 10.3233/FI-2021-2066

Citation: Fundamenta Informaticae, vol. 182, no. 1, pp. 69-94, 2021