Séminaire CONVECS 2022
La Mure (Isère)

Logo CONVECS

 

La Mure

 


Programme scientifique


Mercredi 22 Juin 2022

12h00 – 13h30

Déjeuner et début du séminaire

13h30 – 14h45

Gwen Salaün

Modelling, Analysis, and Optimization of BPMN Processes

 

Business process optimisation is a strategic activity in organizations because of its potential to increase profit margins and reduce operational costs. One of the main challenges in this context is concerned with the problem of optimising the allocation and sharing of resources. In this work, processes are described using the BPMN notation extended with an explicit description of execution time and resources associated with tasks, and can be concurrently executed multiple times. First, a simulation-based approach for computing certain metrics of interest, such as average execution time or resource usage, is presented. This approach applies off-line and is static in the sense that the number of resources does not evolve over the time of the simulation. In a second step, an alternative approach is presented, which works online, thus requiring the instrumentation of an existing platform for retrieving information of interest during the processes' execution. This second approach is dynamic because the number of resource replicas is updated over the time of the execution. Third, we propose a refactoring procedure whose final goal is to reduce the total execution time of the process given as input. This procedure relies on refactoring operations that reorganize the tasks in the process by taking into account the resources used by those tasks.

14h45 – 15h30

Quentin Nivon

Model Checking and Debugging of BPMN Processes using Coloration Techniques

 

For decades, companies have been using the BPMN notation to describe their business processes. In some domains, such as safety-critical systems, companies may need to verify the good behavior of their process with regards to a given temporal logic property. For now, such verifications can mainly be performed using model checking techniques, which verify a property over a model and return a counterexample of the property if it exists. For certain users, such counterexamples can be not helpful, due to their complexity, and the fact that they will not be expressed using the BPMN notation. We propose an approach that aims at representing the counterexample(s) returned by the model checker in BPMN notation.

 

This approach is based on coloration, in which BPMN nodes violating the property are colored in red, while nodes satisfying the property are colored in green. The approach is decomposed in two main parts. In the first one, we try to color the initial BPMN process directly, so that the user gets back its initial BPMN process without any modification. In the second one, in which direct coloration could not be performed, we generate a new BPMN process, semantically equivalent to the first one, and as small in number of tasks as possible.

15h30 – 16h00

Pause café

16h00 – 16h45

Koffi Marck-Edward Kemeh

Synthesis of BPMN with Time and Resources

 

A well-defined business process helps a company's operations to run smoothly. Organizations understand this concept and are constantly working to improve their processes. However, process optimization appears to be a difficult task. It is challenging to collaborate on redesigning an existing process to a better one while taking important factors such as time and resources into account. This gets even more difficult in larger processes that rely on several other operations. In response to this challenge, we propose a method for automatically generating a new process entirely via a procedure known as synthesis.

 

Synthesizing a process also presents some challenges, such as maximizing resource use, but the advantage of this technique is that there is no reference process or set of logs to consider when generating a process. It is considered that no process exists and that a new one is required for a business to begin operations.

 

In this experiment, we take into account the available resource instances or replicas as well as their activity dependency. We also analyze some activity sequences whose execution order must not be modified in order to maintain the process's validity. This is referred to as partial ordering. Following the generation of an ideal process, we proceed to compute the cost in financial terms to establish whether or not utilizing such a process is cost effective. This is because, in order to establish whether a process may raise a company's profit margin, it must be less expensive than a method or process already followed. If the entire execution time can be lowered, the cost margin can be raised. Reducing the overall execution time of a process is dependent on two timing factors: a resource's active and passive time. We analyze these factors to establish their effect on a business.

 

To simplify the synthesis approach, we examine an abstract input that comprises a collection of activities, a set of partial orders, a set of resource instances, and a cost associated with using a resource. Beyond our approach to solving this problem, we explain and present case studies and experiments conducted to evaluate our strategy.

16h45 – 17h30

Ahang Zuo (joint work with Yliès Falcone and Gwen Salaün)

Probabilistic Model Checking of BPMN Processes at Runtime

 

Business Process Model and Notation (BPMN) is a standard business process modelling language that allows users to describe a set of structured tasks, which results in a service or product. Before running a BPMN process, the user often has no clear idea of the probability of executing some task or specific combination of tasks. This is, however, of prime importance for adjusting resources associated with tasks and thus optimising costs. We define an approach to perform probabilistic model checking of BPMN models at runtime. To do so, we first transform the BPMN model into a Labelled Transition System (LTS). Then, by analysing the execution traces obtained when running multiple instances of the process, we can compute the probability of executing each transition in the LTS model, and thus generate a Probabilistic Transition System (PTS). Finally, we perform probabilistic model checking for verifying that the PTS model satisfies a given probabilistic property. This verification loop is applied periodically to update the results according to the execution of the process instances. All these steps are implemented in a tool chain, which was applied successfully to several realistic BPMN processes.

20h00

Dîner

Jeudi 23 Juin 2022

09h00 – 10h00

Radu Mateescu (joint work with Frédéric Lang)

An Update on MCL and Some On-the-Fly Verification Algorithms 

 

On-the-fly verification consists in exploring the LTS (Labelled Transition System) model of a concurrent system incrementally while checking a temporal logic formula. This technique allows the model checker to stop as soon as a diagnostic (witness or counterexample) for the formula has been encountered during the exploration of the LTS. MCL is a language for expressing temporal properties of concurrent value-passing systems. It is based on an extension of the (alternation-free) mu-calculus with data values, modalities containing generalized regular formulas over transition sequences, parameterized fixed point operators, and fairness operators similar to generalized Büchi automata. MCL is equipped with the EVALUATOR model checker of CADP, which uses as verification engine the CAESAR_SOLVE library for on-the-fly resolution of BESs (Boolean Equation Systems). In this talk, we give an overview of MCL and of the on-the-fly verification method used by EVALUATOR, emphasizing recent improvements of some BES resolution algorithms, as well as their application to offline and online trace verification.

10h00 – 10h45

Irman Faqrizal

Probabilistic Model Checking of IEC 61499 Applications

 

Industrial automation is a complex process involving various stakeholders. The international standard IEC 61499 helps to specify distributed automation using a generic architectural model, targeting the technical development of the automation. However, analysing the correctness of IEC 61499 models remains a challenge because of their informal semantics and distributed logic. We introduce new verification techniques for IEC 61499 applications. These techniques combine a design-time analysis for computing a formal model of the application with a runtime analysis for extracting additional information during the execution. This combination of analyses allows for building a richer model of the application and thus formally verifying it using probabilistic model checking. Our approach is fully automated using several tools and was validated on realistic IEC 61499 applications.

10h45 – 11h15

Pause café

11h15 – 12h00

Hubert Garavel (joint work with Pierre Bouvier)

Efficient Algorithms for Three Reachability Problems in Safe Petri Nets

 

We investigate three particular instances of the marking coverability problem in ordinary, safe Petri nets: the Dead Places Problem, the Dead Transitions Problem, and the Concurrent Places Problem. To address these three problems, which are of practical interest, although not yet supported by mainstream Petri net tools, we propose a combination of static and dynamic algorithms. We implemented these algorithms and applied them to a large collection of 13,000+ Petri nets obtained from realistic systems – including all the safe benchmarks of the Model Checking Contest. Experimental results show that 95% of the problems can be solved in a few minutes using the proposed approaches.

12h00 – 14h00

Déjeuner

14h00 – 14h45

Philippe Ledent (joint work with Wendelin Serwe and Radu Mateescu)

Introduction to PSS and translation to LNT

 

Industrial verification of System-on-Chip (SoC) architectures is a very tedious and complex process. The Portable Stimulus Standard (PSS) is a new standard industrial modeling language to describe high-level SoC behavior in view of test generation. Though the language may seem appropriate and adequate from an industrial standpoint, it lacks a native model checker to ensure that the behavior described in the PSS model which will be used to generate tests conforms to the specification. This talk will present PSS and show how CADP can be used for the model checking.  

14h45 – 15h30

Wendelin Serwe (joint work with Philippe Ledent and Radu Mateescu)

Analyzing System-on-Chip Resource Isolation with Formal Test Generation Methods

 

The Internet of Things makes security requirements such as resource isolation ever more necessary, especially at hardware level. Whenever concurrent applications in a System-on-Chip (SoC) have access to shared components, it is crucial to verify that sensitive data stored in these components can only be accessed by authorized applications. The traditional industrial approach is to verify the behavior of each component on its own and then verify the integration of the components into the SoC by exercising each feature at least once through directed tests. However, for security requirements such as resource isolation, this approach might oversee bugs, which could be found if the features were exercised differently.

 

This work applies formal methods to model a complex industrial SoC behavior at a more abstract level, to generate, for each feature, a set of conformance test scenarios, i.e., a set of meaningful directed tests to be exercised on the SoC. The feature in focus is the security requirement of resource isolation at hardware level. The generated tests take into consideration multiple parallel CPUs over which the tests are distributed.

15h30 – 16h00

Pause café

16h00 – 20h00

Quartier libre

20h00

Dîner

Vendredi 24 Juin 2022

09h00 – 09h45

Frédéric Lang (joint work with Luca Di Stefano)

Compositional Verification of Priority Systems using Sharp Bisimulation

 

Sharp bisimulation is a refinement of divergence-preserving branching (a.k.a. divbranching) bisimulation, parameterized by a subset of the system's actions, called strong actions. This parameterization allows the sharp bisimulation to be taylored by the property under verification, whichever property of the modal mu-calculus is considered, while potentially reducing more than strong bisimulation. Sharp bisimulation equivalence is a congruence for parallel composition and other process algebraic operators such as hide, cut, and rename, and hence can be used in a compositional verification setting. In this talk, we show that sharp bisimulation equivalence is also a congruence for action priority operators under some conditions on strong actions. We compare sharp bisimulation with orthogonal bisimulation, whose equivalence is also a congruence for action priority. We show that, if the internal action tau neither yields priority to nor takes priority over other actions, then the quotient of a system with respect to sharp bisimulation equivalence (called sharp minimization) cannot be larger than the quotient of the same system with respect to orthogonal bisimulation equivalence. We then describe a signature-based partition refinement algorithm for sharp minimization, implemented in the BCG_MIN tool of CADP. This algorithm can be adapted to implement orthogonal minimization. We show on a crafted example that using compositional sharp minimization may yield state space reductions that outperform compositional orthogonal minimization by several orders of magnitude. Finally, we illustrate the use of sharp minimization and priority to verify a bully leader election algorithm.

09h45 – 10h30

Lucie Muller (joint work with Wendelin Serwe and Radu Mateescu)

Formal Modeling and Analysis of a Battery Thermal Controller

 

Autonomous vehicles (AV) are complex and critical systems requiring a rigorous design process. The ECSEL project ArchitectECA2030 aims at devising reliable and safer AVs. One of the AV embedded devices considered in this project is a thermal controller in charge of preventing the battery of an electrical car to overheat. In this talk, we will outline the formal modeling of the thermal controller in LNT, the expression of its correctness requirements in MCL, and the (functional and quantitative) analysis we carried out using CADP.

10h30 – 11h00

Pause café

11h00 – 11h45

Jean-Baptiste Horel (joint work with Thomas Genevois and Lucie Muller)

Testing of Perception Systems for Autonomous Vehicles using Augmented Reality on LiDAR Sensors

 

In previous works, we proposed an automatic approach to generate a large number of relevant critical scenarios for autonomous driving simulators. However, simulation testing is not as reliable as real-world testing and performing the scenarios with real vehicles and real obstacles would be too demanding. Therefore, we propose to use a new augmented reality framework that takes advantage of real world and simulation. This new testing methodology is intended to be a bridge between Vehicle-in-the-Loop and real-world testing. It enables to easily and safely place the whole vehicle and all its software, from perception to control, in realistic test conditions. This framework provides a flexible way to introduce any virtual element, such as the obstacles of the scenarios, in the outputs of the sensors of the vehicle under test.

12h00 – 14h00

Déjeuner et fin du séminaire