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 on 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 problematic of the scheduling of a launcher flight control, then we show how this problematic can be formalized with parametric stopwatch automata; we then present the results computed by IMITATOR. We compare the results to the ones obtained by other tools classically used in scheduling.
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 help considering 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 parametrize 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. 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.
The synthesis of controllers for reactive systems can be done by computing winning strategies in two-player games. Timed (game) Automata are an appropriate formalism to model real-time embedded systems but are not easy to use for controller synthesis for two reasons: i) timed models require the knowledge of the precise timings of the system (for example, if an action must occur in the future, the deadline of this occurrence must be known) ii) in practice, the dense state space makes the computation of the controller often impossible for complex systems. This paper introduces an extension of untimed game automata with logical time. The new semantics introduces two new types of uncontrollable actions: delayed actions which are possibly avoidable, and ineluctable actions which will eventually happen if nothing is done to abort it. The controller synthesis problem is adapted to this new semantics. This paper focuses specifically on the reachability and safety objectives and gives algorithms to generate a controller. The usefulness of this new model is illustrated by a device driver synthesis example.
Concurrent data structures provide the means to multi-threaded applications to share data. Typical designs of concurrent data structures are based on locks in order to avoid inconsistency due to concurrent modifications. Locks though introduce a sequential component in Amdahl's law. Lock-free algorithmic designs of concurrent data structures were introduced in the quest for better performance and scalability and are widely used in practice. Lock-free designs typically employ optimistic conflict control making performance analysis challenging. In this talk, I will describe recent efforts in analyzing their performance.
An efficient way to cope with the combinatorial explosion problem induced by the model checking process is to compute the Symbolic Observation Graph (SOG). Given an stuttering invariant event-based LTL formula φ, involving a subset of actions E (called observed actions), the SOG is a condensed representation of the state space graph based on a symbolic encoding of the nodes (sets of states linked with unobserved actions) and an explicit representation of the edges (labelled with observed actions only). It has the advantage to be much reduced comparing to the original state space graph while being equivalent with respect to linear time properties (i.e., the original state space graph satisfies φ if and only if the corresponding SOG satisfies φ). Aiming to go further in the process of tackling the state space explosion problem, we propose in this paper to parallelize the construction of the SOG using a hybrid approach (distributed+shared memory). Doing so, we take advantage of the recent advances in computer hardware, by distributing the construction process over a large number of multi-core processors. We studied the performances of our new approach comparing to both distributed and shared memory approaches on one side, and to the sequential construction of the SOG, on the other hand. The obtained results show that the proposed approach offers an interesting alternative allowing to completely exploit the available distributed architecture while offering significant speedup.
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.
The paper presents the design of a generalised asynchronous arbiter with a two-stage architecture that efficiently handles requests from multiple concurrent channels. The first stage of the arbiter monitors the incoming requests and locks their state as soon as one or more requests are detected. The second stage performs arbitration based on the locked state of the requests and produces the corresponding grant signals. The separation of the two stages is crucial for reducing the complexity of the arbitration logic, which allows us to obtain practical implementations for complex arbitration protocols. Several application examples of the generalised arbiter are proposed and evaluated in terms of scalability with respect to the growing number of request channels. The presented designs are verified to have no hazards or deadlocks using methods based on circuit Petri nets.
Stream programming abstracts parallelism complexity by modeling a program as a set of streaming tasks. Tasks run repeatedly and can even be internally parallel, i.e., use one or multiple cores simultaneously (moldable). The throughput of the streaming application, as well as its energy consumption, depends strongly on scheduling, i.e., on how tasks are mapped to cores, and on the frequency at which they run. Crown scheduling is a scheduling method that reduces this problem's combinatorial complexity considerably by introducing a few additional restrictions especially on tasks' core allocation sizes and mapping. While it has previously been shown to outperform competing methods, the impact of these restrictions on the schedule quality has, up to now, never been analyzed quantitatively. In this paper, we first propose several crown scheduler improvements toward fewer restrictions. Also, we provide an Integer Linear Programming formulation that solves the same optimization problem without the inherent restrictions of crown scheduling. While in an extreme case an unrestricted schedule might use 3.7 times less energy than a crown schedule for a realistic execution platform model, we show that in practical benchmarks the difference is small while crown schedulers are significantly faster than unrestricted scheduling. We experimentally confirm this with benchmarks derived from random task collections, classic parallel algorithms as well as the Streamit benchmark suite.
Relating event data and process models is becoming an important element for organizations. This paper presents a novel approach for aligning traces and process models. The approach is based on the structural theory of Petri nets (the marking equation), applied over an unfolding of the initial process model. Given an observed trace, the approach adopts an iterative optimization mechanism on top of the unfolding, computing at each iteration part of the resulting alignment. In contrast to the previous work that is primarily grounded in the marking equation, this approach is guaranteed to provide real solutions, and tries to mimic as much as possible the events observed in the trace. Experiments witness the significance of this approach both in quality and execution time perspectives.
Synchronous control asynchronous dataflow (SCAD) architectures are a new kind of exposed datapath processor architectures which reveal all of their processing units (PU) and datapaths to the compiler to increase the use of instruction-level parallelism (ILP). They employ FIFO buffers at the input and output ports of their PUs, consuming operands and producing results similar to dataflow computers. Because the arrival of operands triggers the execution of instructions, SCAD architectures only need a single type of instruction that transports data from output buffers to input buffers. Among other advantages, this allows a simple integration of application-specific PUs, since a PU may implement in principle any function that can be realized with reasonable hardware without changing the instruction set. However, simply allowing any computable function for PUs introduces problems: Because of the asynchronous nature of data moves and operation execution, not all functions yield scheduling-independent, deterministic results. In this paper, we therefore first describe an operational semantics for SCAD architectures which enables formal reasoning about the underlying model of computation. Then, we create an equivalent model using well-known dataflow process networks. From this model, the desired restrictions for functions can then be derived, giving a configurable and sound class of SCAD architectures. Finally, we discuss further restrictions that should be applied and propose a notion for well-structured SCAD machine code.
Threads are a wildly non-deterministic model of computation, difficult to analyze in the general case (the wolf of our title). But when system specification is a deterministic dataflow program written in Lustre, Scade or Simulink, the implementation process should build not just multi-threaded C code, but (first and foremost) a richer model exposing the easy-to-analyze dataflow, race-free organization of the computations performed by the implementation (the titular sheep). We propose a language for such implementation models. It allows the formulation of functional correctness properties the multi-threaded implementation must satisfy for an avionics use case running on a commercial many-core.
The world of project management (PM) is diverse and extensive, as is the resulting tool selection on the market. Despite the wide variety of tools available, many PM activities are carried out using self-developed spreadsheets that have been tailored to meet the needs of the project. The authors have evaluated experiences from several completed projects and recognizes the need for a systematic model based on a formalised and tool-independent table structure. The goal of this work is to use a powerful Petri net (PN) model for mapping and simulation, taking advantage of the model’s benefits. Thus, an effective and flexible methodology for PM can be realised. In order to use the concept of PN for this purpose, appropriated extensions and necessary interpretations from the area of high-level timed Petri nets must be used. Moreover, PM has to be brought to the same description level as PN. The concept of this proposed method is to enter all data, initial plan inputs and intermediate status updates into a defined table structure. A PN is then automatically generated in the background or updated to reflect the current status of the project. Simulations should be performed on the PN models, and their results should be put back into the table. The advantages of the PN concept can thus be fully exploited and become useful for a project manager, even if he or she does not have any PN knowledge. This article presents an overview of the proposed formalised methodology, its suitability to PM, and its benefits. The method itself can be applied to a wide range of projects. Focus is placed on how to transfer certain areas of PM into the introduced PN constructs and interfaces. Examples are used to illustrate how to transform PM activities and their related information into the selected PNs.
Today, serious warnings regarding the increasing number of DNS tunnelling methods are on the rise. Attackers have used such techniques to steal data from millions of accounts. The existing literature has thoroughly demonstrated the extent of the damage which DNS tunnelling can achieve on any given DNS server. However, through SONs Petri net-based formalisms which portray the behaviour of complex evolving systems, such threats can be alleviated. As a concept, SONs are originally grounded in Occurrence Nets (ONs) and already yielded results in terms of successful cybercrime analysis. For instance, adding of alternates to SONs initially used in [10] was extended to in [15] in order to model and analyse system activities such as cybercrime or accidents, which may show contradictory or uncertain evidence in terms of actual activity. The current paper proposes the use of SON features with the purpose of detecting DNS tunnelling, in the event of an actual attack.
Work funded by the Spanish Ministry of Science (project MASSIVE, RTI2018-095255- B-I00) and the R&D programme of Madrid (project FORTE, P2018/TCS-4314)
Too much effort is being invested in the automated planning field, but this area has been focusing more on improving the performance of search algorithms in an abstract space than on applying automated planning in practice. Among several challenges, online replanning is an open issue. This paper presents PNRD/iPNRD integration in Blocks World Domain in order to create an adaptive control of a robotic arm and passive agents. The procedure is composed of building a Petri space, PNRD, and iPNRD model for each agent, and by integrating their information so that the robotic arm may autonomously order the blocks to the desired final global state, stored previously in each block’s RFID tag; comparing logical and physical information, generating a sequence of movements, and executing related actions. Some issues arise because of the dispersed information, physical-logical interface and its constraints, requiring the detection of non-conformant results, optimally solve and realize the required sorting given its partial observability, and sequential movement of one block each time. The feedback from PNRD/iPNRD models with physical positioning can certify the required initial, intermediate and final condition and also check for exceptions, resulting in an adaptive robotic control. This didact example points out where this approach can work with automated planning for a more complex system.
