|
Séminaire CONVECS 2022 |
|
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 |
|