Specification and Verification Seminar

The specification and verification seminar happens on Thursdays at 3.30pm, so far at least once every two weeks. We usually meet at the seminar room, B107.

In this page you will find the abstracts and seminar materials of previous sessions. Anounces of forthcoming seminars are made on this page.

Contact: César Rodríguez.



CARET Model Checking For Pushdown Systems

Date:
March 23, 2017
Speaker:
Huu-Vu Nguyen, LCR, LIPN, Paris 13
Abstract:

CARET (A temporal logic of calls and returns) was introduced by Alur et al. This logic allows to write linear temporal logic formulas while taking into account matching of calls and returns. However, CARET model checking for Pushdown Systems (PDSs) was never considered in the literature. Previous works only dealt with the model checking problem for Recursive State Machine (RSMs). While RSMs are a good formalism to model sequential programs written in structured programming languages like C or Java, they become non suitable for modeling binary or assembly programs, since, in these programs, explicit push and pop of the stack can occur. Thus, it is very important to have a CARET model checking algorithm for PDSs. We tackle this problem in this paper. We also consider CARET model checking with regular valuations, where the set of configurations in which an atomic proposition holds is a regular language. We reduce these problems to the emptiness problem of Büchi Pushdown Systems. We implemented our technique in a tool, and we applied it to different case studies. Our results are encouraging. In particular, we were able to apply our tool to detect several malwares.

This is a joint work with Tayssir Touili.

Materials:
Slides available (soon) here.

Preserving Partial Order Runs in Parametric Time Petri Nets

Date:
March 16, 2017
Speaker:
César Rodríguez, LCR, LIPN, Paris 13
Abstract:

Parameter synthesis for timed systems aims at deriving parameter valuations satisfying a given property. In this paper we target concurrent systems; it is well known that concurrency is a source of state-space explosion, and partial order techniques were defined to cope with this problem. Here we use partial order semantics for parametric time Petri nets as a way to significantly enhance the result of an existing synthesis algorithm. Given a reference parameter valuation, our approach synthesizes other valuations preserving, up to interleaving, the behavior of the reference parameter valuation. We show the applicability of our approach using acyclic asynchronous circuits.

Join work with Thomas Chatain and Étienne André.

Materials:
Slides available here.

Hybride Modelling, Analysis and Quantitative Verification of Large Biological Regulatory Networks

Date:
March 9, 2017
Speaker:
Louis Fippo Fitime, LCR, LIPN, Paris 13
Abstract:

Biological Regulatory Networks (BRNs) are usually used in systems biology for modelling, understanding and controlling the dynamics of different biological functions (differentiation, proliferation, proteins synthesis, apoptose) inside cells. Those networks are enhanced with experimental data that are nowadays more available which give an idea on the dynamics of BRNs components. Formal analysis of such models fails in front of the combinatorial explosion of generated behaviours despite the fact that BRNs provide abstract representation of biological systems.

This thesis handles hybrid modelling, the simulation, the formal verification and control of Large Biological Regulatory Networks. This modelling is done thanks to stochastic automata networks, thereafter to Process Hitting by integrating time-series data.

Firstly, this thesis proposes a refining of the dynamics by estimation of stochastic and temporal (delay) parameters from time-series data and integration of those parameters in automata networks models. This integration allows the parametrisation of the transitions between the states of the system. Then, a statistical analysis of the traces of the stochastic simulation is proposed to compare the dynamics of simulations with the experimental data.

Secondly, this thesis develops static analysis by abstract interpretation in the automata networks allowing efficient under- and over-approximation of quantitative (probability and delay) reachability properties. This analysis enables to highlight the critical components to satisfy these properties.

Finally, taking advantage from the previous developed static analyses for the reachability properties in the qualitative point of view, and from the power of logic programming (Answer Set Programming), this thesis addresses the domain of control of system by proposing the identification of bifurcation transitions. Bifurcations are transitions after which the system can no longer reach a state that was previously reachable.

Keywords:
complex systems; biological regulatory networks; hybrid modelling; data integration; stochastic simulation; static analysis; formal verification; abstract interpretation; bifurcation; control.
Materials:
Slides available here.

Reachability Analysis of Pushdown Systems with an Upper Stack

Date:
March 2, 2017
Speaker:
Adrien Pommellet, LCR, LIPN, Paris 13
Abstract:

Pushdown systems (PDSs) are a natural model for sequential programs, but they can fail to accurately represent the way an assembly stack actually operates. Indeed, one may want to access the part of the memory that is below the current stack or base pointer, hence the need for a model that keeps track of this part of the memory. To this end, we introduce pushdown systems with an upper stack (UPDSs), an extension of PDSs where symbols popped from the stack are not destroyed but instead remain just above its top, and may be overwritten by later push rules.

We prove that the sets of successors post* and predecessors pre* of a regular set of configurations of such a system are not always regular, but that post* is context-sensitive, so that we can decide whether a single configuration is forward reachable or not. In order to underapproximate pre* in a regular fashion, we consider a bounded-phase analysis of UPDSs, where a phase is a part of a run during which either push or pop rules are forbidden. We then present a method to overapproximate post* that relies on regular abstractions of runs of UPDSs. Finally, we show how these approximations can be used to detect stack overflows and stack pointer manipulations with malicious intent.

This is a joint work with Marcio Diaz And Tayssir Touili.

Materials:
Slides available (soon) here.

Malware Detection Based On Graph Classification

Date:
February 9, 2017
Speaker:
Khanh-Huu-The Dam, LCR, LIPN, Paris 13
Abstract:

Malware detection is nowadays a big challenge. The existing techniques for malware detection require a huge effort of engineering to manually extract the malicious behaviors. To avoid this tedious task of manually discovering malicious behaviors, we propose in this paper to apply learning for malware detection.

Given a set of malwares and a set of benign programs, we show how learning techniques can be applied in order to detect malware. For that, we use abstract API graphs to represent programs. Abstract API graphs are graphs whose nodes are API functions and whose edges represent the order of execution of the different calls to the API functions (i.e., functions supported by the operating system). To learn malware, we apply well-known learning techniques based on Random Walk Graph Kernel (combined with Support Vector Machines). We can achieve a high detection rate with only few false alarms (98.93% for detection rate with 1.24% of false alarms). Moreover, we show that our techniques are able to detect several malwares that could not be detected by well-known and widely used antiviruses such as Avira, Kaspersky, Avast, Qihoo-360, McAfee, AVG, BitDefender, ESET-NOD32, F-Secure, Symantec or Panda.

This is a joint work with Tayssir Touili.

Materials:
Slides available (soon) here.

What’s decidable about parametric timed automata?

Date:
January 19, 2017
Speaker:
Étienne André, LCR, LIPN, Paris 13
Abstract:
Parametric timed automata (PTA) are a powerful formalism to reason, simulate and formally verify critical real-time systems. After two decades of research on PTA, it is now well-understood that any non-trivial problem studied is undecidable for general PTA. We provide here a survey of decision and computation problems for PTA. On the one hand, bounding time, bounding the number of parameters or the domain of the parameters does not (in general) lead to any decidability. On the other hand, restricting the number of clocks, the use of clocks (compared or not with the parameters), and the use of parameters (e.g. used only as upper or lower bounds) leads to decidability of some problems.
Materials:
Slides available here.

Parametric model checking timed automata under non-Zenoness assumption

Date:
January 12, 2017
Speaker:
Hoang Gia Nguyen, LIPN, Université Paris 13
Abstract:
Real-time systems often involve hard timing constraints and concurrency, and are notoriously hard to design or verify. Given a model of a real-time system and a property, parametric model-checking aims at synthesizing timing valuations such that the model satisfies the property. However, the counter-example returned by such a procedure may be Zeno (an infinite number of discrete actions in a finite time), which is unrealistic. On the one hand, we show that synthesizing parameter valuations such that at least one counter-example run is non-Zeno is undecidable for Parametric Timed Automata (PTA). On the other hand, we propose a procedure based on a transformation of PTA into Clock Upper Bound PTA to derive such valuations.
Materials:
Slides available here.

Harnessing Malware Intelligence for Defense and Attribution

Date:
January 12, 2017
Speaker:
Arun Lakhotia, Cythereal; University of Louisiana at Lafayette
Abstract:

The number of unique malware has been doubling every year for over two decades. The majority of effort in malware analysis has focused on methods for preventing malware infection. We view the exponential growth of malware as an underutilized source of intelligence. Given that the number of malware authors are not doubling each year, the large volume of malware must contain evidence that connects them. The challenge is how to extract the connections and do so in a timely manner to be useful.

This talk will describe Cythereal MAGIC, a cloud-based malware analysis service, for mining large scale malware repositories. MAGIC, an offshoot of research conducted under the DARPA Cyber Genome program, uses malware "genome" to construct features that are resilient to many obfuscations. The correlations discovered by MAGIC can be used to prevent and detect zero-day malware. The correlations can also be used to investigate malware attacks for attribution.

Bio :
Dr. Arun Lakhotia is a Professor of Computer Science at the University of Louisiana at Lafayette, and the Director of Software Research Laboratory, and Founder/CEO of Cythereal, Inc. His research, supported in part by the DARPA Cyber Genome program, led to the development of VirusBattle, an automated malware analysis web service that draws connections between malware using the semantics of their underlying code. Lakhotia founded Cythereal to commercialize VirusBattle. Cythereal produces Malware Genomic Correlations (MAGIC) analysis aimed at helping organizations prevent, defend, and investigate zero-day malware attacks. Dr. Lakhotia earned his PhD in Computer Science from Case Western Reserve University in 1990. He is the recipient of the 2004 Louisiana Governor's Technology Leader of the Year Award.
Materials:
Slides available (soon) here.

Proving array-manipulating programs without arrays

Date:
December 2, 2016
Speaker:
David Monniaux, VERIMAG, Université de Grenoble
Abstract:

Automatically verifying safety properties of programs is hard. Many approaches exist for verifying programs operating on Boolean and integer values (e.g. abstract interpretation, counterexample-guided abstraction refinement using interpolants), but transposing them to array properties has been fraught with difficulties. Our work addresses that issue with a powerful and flexible abstraction that morphes concrete array cells into a finite set of abstract ones. This abstraction is parametric both in precision and in the back-end analysis used.

One possible application would be distributed systems, where processes are modeled using arrays indexed by the process ID.

Materials:
Slides available here.

Approches pour la modélisation et vérification des systèmes temporisés en utilisant les diagrammes états-transitions et les réseaux de Petri colorés

Date:
December 1, 2016
Speaker:
Mahdi Benmoussa, LCR, LIPN, Paris 13
Abstract:

Nous présentons dans ce travail de thèse des approches pour la spécification et la vérification des systèmes temporisés. La première partie concerne une méthode de spécification en utilisant les diagrammes états-transitions pour modéliser un système donné en partant d'une description textuelle. Elle comporte plusieurs étapes et utilise des observateurs d'états et des événements afin d'engendrer le diagramme états-transitions. Un outil qui implémente les différentes étapes de la méthode de spécification pour une application semi-automatique est présenté. La seconde partie concerne une traduction des diagrammes états-transitions vers les réseaux de Petri colorés, ce qui permet d'utiliser les méthodes de vérification. Nous prenons en considération dans cette traduction un ensemble important des éléments syntaxiques des diagrammes états-transitions, tels que la concurrence, la hiérarchie, etc. Un outil qui implémente la traduction pour un passage automatique des diagrammes états-transitions vers les réseaux de Petri colorés est en cours de développement. La dernière partie concerne l'intégration des contraintes temporelles dans les deux approches précédentes. Nous définissons des annotations pour les diagrammes états-transitions dont nous fournissons la syntaxe et la sémantique. Ces annotations seront ensuite utilisées dans la méthode de spécification et la traduction. Le but est de proposer des annotations faciles à comprendre et à utiliser avec une syntaxe qui prend en compte des contraintes parmi les plus utilisées.

Mots clés : modélisation, diagrammes états-transitions UML, formalisation, sémantique formelle, réseaux de Petri colorés, contraintes temporelles.

Materials:
Slides available (soon) here.

Integer-Complete Synthesis for Bounded Parametric Timed Automata

Date:
October 20, 2016
Speaker:
Étienne André, LCR, LIPN, Paris 13
Abstract:

Ensuring the correctness of critical real-time systems, involving concurrent behaviors and timing requirements, is crucial. Parameter synthesis aims at computing dense sets of valuations for the timing requirements, guaranteeing a good behavior. However, in most cases, the emptiness problem for reachability (i.e. whether there exists at least one parameter valuation for which some state is reachable) is undecidable and, as a consequence, synthesis procedures do not terminate in general, even for bounded parameters. In this paper, we introduce a parametric extrapolation, that allows us to derive an underapproximation in the form of linear constraints containing all the integer points ensuring reachability or unavoidability, and all the (non-necessarily integer) convex combinations of these integer points, for general PTA with a bounded parameter domain. Our algorithms terminate and can output constraints arbitrarily close to the complete result.

Joint work with Didier Lime and Olivier H. Roux.

Materials:
Slides available here.

Automatic Extraction of Malicious Behaviors

Date:
October 6, 2016 (at 1pm instead of 2pm)
Speaker:
Khanh-Huu-The Dam, LCR, LIPN, Paris 13
Abstract:

The number of new malwares is increasing everyday. Thus malware detection is nowadays a big challenge. The existing techniques for malware detection require a huge effort of engineering to manually extract the malicious behaviors. To avoid this tedious task, we propose in this paper an approach to automatically extract the malicious behaviors. We model a program using an API call graph, and we represent the malicious behaviors using a malicious API graph. We then reduce the malicious behavior extraction problem to the problem of retrieving from the benign and malicious API call graphs the set of subgraphs that are relevant for malicious behaviors. We solve this issue by applying and adapting well-known efficient Information Retrieval techniques based on the TFIDF scheme. We use our automatically extracted malicious behavior specification for malware detection using a kind of product between graphs. We obtained interesting experimental results, as we get 99.04% of detection rate. Moreover, we were able to detect several malwares that well-known and widely used antiviruses such as Panda, Avira, Kaspersky, Avast, Qihoo- 360, McAfee, AVG, BitDefender, ESET-NOD32, F-Secure, and Symantec could not detect.

This is a joint work with Tayssir Touili.

Materials:
Slides available: PPTX (original), PDF (converted).

Parameter Synthesis for Parametric Interval Markov Chains

Date:
Mars 3, 2016
Speaker:
Laure Petrucci, LCR, LIPN, Paris 13
Abstract:

Interval Markov Chains (IMCs) are the base of a classic probabilistic specification theory introduced by Larsen and Jonsson in 1991. They are also a popular abstraction for probabilistic systems. In this paper we study parameter synthesis for a parametric extension of Interval Markov Chains in which the endpoints of intervals may be replaced with parameters. In particular, we propose constructions for the synthesis of all parameter values ensuring several properties such as consistency and consistent reachability in both the existential and universal settings with respect to implementations. We also discuss how our constructions can be modified in order to synthesise all parameter values ensuring other typical properties.

Joint work with Benoît Delahaye and Didier Lime.

Materials:
Slides available (soon) here.

Timed Aggregate Graph : a finite graph for model checking of Time Petri Nets

Date:
Feb. 11, 2016
Speaker:
Amal Chamakh, LCR, LIPN, Paris 13
Abstract:
Time Petri Nets (TPNs) are one of the most powerful formalisms for the specification and the verification of systems involving explicit timing constraints. To deal with model checking of timed systems modeled by TPNs, we propose a new finite graph, called Timed Aggregate Graph (TAG), abstracting the behavior of bounded TPNs with strong time semantics. The main feature of this abstract representation compared to existing approaches is the encoding of the time information. This is done in a pure way within each node of the TAG allowing to compute the minimum and maximum elapsed time in every path of the graph. The TAG preserves timed traces and reachable states of the corresponding TPN and allows for on-the-fly verification of reachability properties. We also introduce an algorithm for a modular construction of the TAG, to better confine the state explosion problem.
Materials:
Slides available here.

Unfolding-based Partial Order Reduction

Date:
Feb. 4, 2016
Speaker:
César Rodríguez, LCR, LIPN, Paris 13
Abstract:

Partial order reduction (POR) and net unfoldings are two alternative methods to tackle state-space explosion caused by concurrency. In this paper, we propose the combination of both approaches in an effort to combine their strengths. We first define, for an abstract execution model, unfolding semantics parameterized over an arbitrary independence relation. Based on it, our main contribution is a novel stateless POR algorithm that explores at most one execution per Mazurkiewicz trace, and in general, can explore exponentially fewer, thus achieving a form of emph{super-optimality}. Furthermore, our unfolding-based POR copes with non-terminating executions and incorporates state-caching. On benchmarks with busy-waits, among others, our experiments show a dramatic reduction in the number of executions when compared to a state-of-the-art DPOR.

Joint work with Marcelo Sousa, Subodh Sharma, and Daniel Kroening. Paper available at: http://arxiv.org/abs/1507.00980

Materials:
Slides available here, and Promela example.

Action synthesis for branching time logic: theory and applications

Date:
July. 2, 2015
Speaker:
Michał Knapik, Instytut Podstaw Informatyki, Polskiej Akademii Nauk, Poland
Abstract:
Action-Restricted Computation Tree Logic (ARCTL) is a simple extension of CTL, proposed by Pecheur and Raimondi, where the actions allowed along the considered runs can be explicitly indicated by path selectors. ARCTL allows to express properties such as "a safe state is unavoidable for every path built from Forward and Left actions", denoted by AF{Forward,Safe}safe. By replacing the concrete sets of actions with free variables we obtain a parametric version of the logic pmARCTL, where properties such as AF{X}safe are allowed, where X is a parameter. We introduce a fixed-point theory that allows for the exhaustive synthesis of all the valuations of the variables which make the pmARTCL formulae hold in a given model. The theory has been implemented in an open source stand-alone tool and evaluated on scalable examples with promising results.

BE-PUM: A tool of Binary Emulation for Pushdown Model generation

Date:
June. 29, 2015
Speaker:
Quan Thanh Tho, Ho Chi Minh City University of Technology, Vietnam
Abstract:
In this talk, we present the tool BE-PUM (Binary Emulation for PUshdown Model generation) for binary analysis. As suggested by its name, BE-PUM generates pushdown model, which is considered as a control flow graph (CFG) combined with a memory execution model. BE-PUM also introduces a concolic approach in order to generate CFG in a more precise manner. As such, BE-PUM is able to handle various popular obfuscation techniques of malwares, such as indirect jump or self- modification code. In experiments, we are able to produce models for around 1700 samples of real malware. Compared to JakStab and IDA Pro, two state-of-the-art tools in this field, BE-PUM shows better tracing ability, sometimes with significant differences.

Model-checking for efficient malware detection

Date:
June. 18, 2015
Speaker:
Tayssir Touili, LIPN, Université Paris 13
Abstract:
The number of malware is growing extraordinarily fast. Therefore, it is important to have efficient malware detectors. Malware writers try to obfuscate their code by different techniques. Many of these well-known obfuscation techniques rely on operations on the stack such as inserting dead code by adding useless push and pop instructions, or hiding calls to the operating system, etc. Thus, it is important for malware detectors to be able to deal with the program's stack. In this talk I will show a new model-checking approach for malware detection that takes into account the behavior of the stack. Our approach consists in : (1) Modeling the program using a Pushdown System (PDS). (2) Introducing new logics, called SCTPL and SLTPL, to represent the malicious behavior. SCTPL (resp. SLTPL) can be seen as an extension of the branching-time temporal logic CTL (resp. the linear-time temporal logic LTL) with variables, quantifiers, and predicates over the stack. (3) Reducing the malware detection problem to the model-checking problem of PDSs against SCTPL/SLTPL formulas. We show how our new logics can be used to precisely express malicious behaviors that could not be specified by existing specification formalisms. We then consider the model-checking problem of PDSs against SCTPL/SLTPL specifications. We provide efficient algorithms to solve these problems. We implemented our techniques in a tool, and we applied it to detect several viruses. Our results are encouraging. In particular, our tool was able to detect more than 800 viruses. Several of these viruses could not be detected by well-known anti-viruses such as Avira, Avast, Norton, Kaspersky and McAfee.

Reachability Preservation Based Parameter Synthesis for Timed Automata

Date:
May. 21, 2015
Speaker:
Étienne André, LIPN, Université Paris 13
Abstract:
The synthesis of timing parameters consists in deriving conditions on the timing constants of a concurrent system such that it meets its specification. Parametric timed automata are a powerful formalism for parameter synthesis, although most problems are undecidable. We first address here the following reachability preservation problem: given a reference parameter valuation and a (bad) control state, do there exist other parameter valuations that reach this control state iff the reference parameter valuation does? We show that this problem is undecidable, and introduce a procedure that outputs a possibly underapproximated answer. We then show that our procedure can efficiently replace the behavioral cartography to partition a bounded parameter subspace into good and bad subparts; furthermore, our procedure can even outperform the classical bad-state driven parameter synthesis semi-algorithm, especially when distributed on a cluster.
Materials:
Slides available here.

Formalising Concurrent UML State Machines Using Coloured Petri Nets

Date:
April 16, 2015
Speaker:
Mahdi Benmoussa LIPN, Université Paris 13
Abstract:
While UML state machines are widely used to specify dynamic systems behaviours, their semantics is described informally, which prevents the complex systems verification. In this paper, we propose a formalisation of concurrent UML state machines using coloured Petri nets. We consider in particular concurrent aspects (orthogonal regions, forks, joins, shared variables), the hierarchy induced by composite states and their associated activities, internal/external/local transitions, and entry/exit/do behaviours.
Materials:
Slides available here.

Enhanced Distributed Behavioral Cartography of Parametric Timed Automata

Date:
April 9, 2015
Speaker:
Hoang Gia Nguyen, LIPN, Université Paris 13
Abstract:
Parametric timed automata (PTA) allow the specification and verification of timed systems incompletely specified, or subject to future changes. The behavioral cartography splits the parameter space of PTA in tiles in which the discrete behavior is uniform. Applications include the optimization of timing constants, and the measure of the system robustness w.r.t. the untimed language. Here, we present enhanced distributed master-worker algorithms to compute the cartography efficiently. Experimental results show that our new algorithms significantly outperform previous distribution techniques.
Materials:
Slides available here.

Effective verification of low-level software with nested interrupts

Date:
Mars 19, 2015
Speaker:
Lihao Liang, Department of Computer Science, University of Oxford, UK
Abstract:

Interrupt-driven software is difficult to test and debug, especially when interrupts can be nested and subject to priorities. Interrupts can arrive at arbitrary times, leading to an explosion in the number of cases to be considered. We present a new formal approach to verifying interrupt-driven software based on symbolic execution. The approach leverages recent advances in the encoding of the execution traces of interacting, concurrent threads. We assess the performance of our method on benchmarks drawn from embedded systems code and device drivers, and experimentally compare it to conventional formal approaches that use source-to-source transformations. Our experimental results show that our method significantly outperforms conventional techniques. To the best of our knowledge, our technique is the first to demonstrate effective formal verification of low-level embedded software with nested interrupts.

Joint work with Daniel Kroening, Tom Melham, Peter Schrammel and Michael Tautschnig

Materials:
Slides available here.

Building Bridges Between Sets of Partial Orders

Date:
Mars 12, 2015
Speaker:
Hernán Ponce de León, Department of Information and Computer Science, Aalto University (Finland)
Abstract:

Partial orders are a fundamental mathematical structure capable of representing concurrency and causality on a set of atomic events. In many applications it is essential to consider multiple partial orders, each representing a particular behavioral scenario or an operating mode of a modeled system.

In this talk I will present two mathematical formalisms capable of the compressed representation of sets of partial orders: Labeled Event Structures (LESs) and Conditional Partial Order Graphs (CPOGs). I will demonstrate their advantages and disadvantages and propose efficient algorithms for transforming of a set of partial orders from a given compressed representation in one formalism into an equivalent representation in another formalism without the explicit enumeration of each scenario. These algorithms make use of an intermediate mathematical formalism, which we call Conditional Labeled Event Structures (CLESs), that combines the advantages of LESs and CPOGs.

This is joint work with Andrey Mokhov (Newcastle University)

Materials:
Slides available here.

On an Extension of Freeze LTL with Ordered Attributes

Date:
Mars 4, 2015
Speaker:
Normann Decker, Institute for Software Engineering and Programming Languages, University of Lübeck (Germany)
Abstract:
We present an extension of Freeze LTL, a temporal logic equipped with registers, over data words. Each position in a (multi-attributed) data word carries a letter from a finite alphabet and assigns a data value to a fixed, finite set of attributes. While reasoning on collections of data values is valuable for expressing correctness properties of executions of dynamic programs the satisfiability problem of Freeze LTL is undecidable if more than one register is available or tuples of data values can be stored and compared arbitrarily. Our extension therefore allows for specifying a dependency relation on attributes. These dependencies introduce a restricted, yet flexible way of storing and comparing collections of attribute values. This new dimension of flexibility is orthogonal to, e.g., the number of registers or the available temporal operators. In this setting we characterise precisely the type of dependency relations that maintain decidability of the logic. To this end, we employ reductions from and to nested counter systems. Moreover, by a complexity theoretic characterisations we can show that our extension is strict and induces a semantic hierarchy of logical fragments.
Materials:
Slides available here.

Modelling Timed Concurrent Systems Using Activity Diagram Patterns

Date:
Feb. 19, 2015
Speaker:
Étienne André, LIPN, Université Paris 13
Abstract:

UML is the de facto standard for modelling concurrent systems in the industry. Activity diagrams allow designers to model workflows or business processes. Unfortunately, their informal semantics prevents the use of automated verification techniques. In this paper, we first propose activity diagram patterns for modelling timed concurrent systems; we then devise a modular mechanism to compose timed diagram fragments into a UML activity diagram that also allows for refinement, and we formalise the semantics of our patterns using time Petri nets. Our approach guides the modeller task% (helping to avoid common mistakes), and allows for automated verification.

Joint work with Christine Choppy and Thierry Noulamo

Materials:
Slides available here.

Specification and verification of Time Petri Nets with Coq

Date:
Jan. 22, 2015
Speaker:
Amal Chamakh, LIPN, Université Paris 13
Abstract:
Model checking and theorem proving, have long reached their limitation as general-purpose techniques, and most of the research now is concentrated on efficient specialization of both approaches to relatively narrow problem domains. The state space explosion problem leaves little hope for automatic finite-state verification techniques like model checking to remain practical, especially when designs become parameterized. The use of theorem proving techniques is inevitable to cope with the new verification challenges. "Pure" theorem proving, on the other hand, can also be quite tedious and impractical for complex designs. Ideally, one would like to find an efficient combination of model checking and theorem proving, and the quest for such a combination has long been one of the major challenges in the field of formal verification. In this paper, we address the combination of model checking and theorem proving approaches in order to specify and to model check Time Petri Nets (TPN) model-based systems. In particular, we show how a TPN is specified using the Coq proof assistant, and how the fireability/unfireability of a timed sequence of transitions can be proved. This allows, for instance, to prove the reachability of a given state by the firing of a given timed/untimed trace or to prove that a counter-example supplied by a given (untimed) model checker is a real counterexample of a timed system. %First, we provide a formalization of the net model in COQ via the parsing of its Petri Net Markup Language (PNML) description. Then the COQ proof assistant is used to prove the firability (or the opposite) of traces given by model checking as a counter-example when a propriety being checked is found to be non-valid, hence, states reachability is proved.
Materials:
Slides available here.

Cost Linear Temporal Logic for Verification

Date:
Jan. 14, 2015
Speaker:
Maximilien Colange, CUI Université de Genève
Abstract:

Qualitative formal verification aims at checking that a given formal property holds on a model, given as an automaton. The automata-based approach expresses the property as an automaton then analyses its synchronisation with the model automaton. This method can be extended with various automata flavors to handle quantitative properties.

We focus on an extension of Linear Temporal Logic (LTL) with counting capabilities: Cost Linear Temporal Logic (CLTL). This logics can be translated into Büchi automata equipped with counters, so as to nicely extend the automata approach to model-checking. We describe the new properties that this extension allows to handle, illustrated with examples. We also explain how it is linked to existing qualitative LTL model-checking, and the new challenges it poses. We also propose a CEGAR-like approach to answer compute the bounds of the values reached by the automata.

Materials:
Slides available here.

Teaching Formal Methods: Experience at UPMC and UP13 with CosyVerif

Date:
Dec. 18, 2014
Speaker:
Laure Petrucci, LIPN, Université Paris 13
Abstract:

Nowadays, students are more and more demanding for practical coursework, which is a challenge when teaching formal approaches to software engineering. The solution is to provide environments for such hands-on sessions and homework, but this raises numerous difficulties. The environment must be: (i) multi-platform (Mac OS, Linux, Windows) so as to enable student practice at home, (ii) easy to deploy, (iii) easy to use and to take charge of, and (iv) flexible enough to enable the integration of new notations and associated services.

CosyVerif is a software environment dedicated to graphical notations, that provides the mechanisms and means for an easy integration of additional existing software for teaching (or demonstration) purposes. This makes it an interesting platform to establish new courses.

This paper presents our experience using CosyVerif for teaching Petri nets and parametric timed automata in two universities of the Paris region, i.e. Université Pierre et Marie Curie, and Université Paris 13. We also use CosyVerif to build demonstrators of Ph.D. students' work.

Materials:
Slides available here.

CosyVerif: An Open Source Extensible Verification Environment

Date:
Dec. 11, 2014
Speaker:
Étienne André, LIPN, Université Paris 13
Abstract:

Over the past two decades, numerous verification tools have been successfully used for verifying complex concurrent systems, modelled using various formalisms. However, it is still hard to coordinate these tools since they rely on such a large number of formalisms. Having a proper syntactical mechanism to interrelate them through variability would increase the capability of effective integrated formal methods. Here, we propose a modular approach for defining new formalisms by reusing existing ones and adding new features and/or constraints. Our approach relies on standard XML technologies; their use provides the capability of rapidly and automatically obtaining tools for representing and validating models. It thus enables fast iterations in developing and testing complex formalisms. As a case study, we applied our modular definition approach on families of Petri nets and timed automata. This work is implemented in the CosyVerif platform, a modular framework integrating verification software tools of the Paris region.

This is a joint work with the CosyVerif team.

Materials:
Slides available here.

Precise Robustness Analysis of Real-Time Systems

Date:
Nov. 27, 2014
Speaker:
Étienne André, LIPN, Université Paris 13
Abstract:

Quantifying the robustness of a real-time system consists in measuring the maximum extension of the timing delays such that the system still satisfies its specification. In this work, we introduce a more precise notion of robustness, measuring the allowed variability of the timing delays in their neighbourhood. We consider here the formalism of time Petri nets extended with inhibitor arcs. We use the inverse method, initially defined for timed automata. Its output, in the form of a parametric linear constraint relating all timing delays, allows the designer to characterise the system local robustness, and hence to identify the delays allowing the least variability. We also exhibit a condition and a construction for rendering robust a non-robust system.

This work is a joint work with Laure Petrucci.

Materials:
Slides available here.

Abstraction and Modular Verification of Services Using Symbolic Observation Graph (SOG)

Date:
Nov. 20, 2014
Speaker:
Hanene Ochi, LIPN, Université Paris 13
Abstract:
For automatically composing services in a correct manner, information about their behaviors (an abstract model) has to be published in a repository. This abstract model must be sufficient to decide whether two, or more, services are compatible (the composition is possible) without including any additional information that can be used to disclose the privacy of these services. The compatibility between two services can be based either on some generic properties or specific ones . This talk will present my work during my thesis about the problem considering these kinds of compatibility criteria, and we will introduce approches for the automatic abstraction of services and to the modular checking of their compatibility using their abstract models only. To abstract services, we use the symbolic observation graph (SOG) approach that preserves necessary informa tion for service composition and hides private information. We will show how the SOG can be adapted and used so that the verification of generic and specific compatibility criteria can be performed on the composition of the abstract models of services instead of the original composite service.
Materials:
Slides available here.

Introduction to Partial Order Reductions

Date:
Nov. 6, 2014
Speaker:
César Rodríguez, LIPN, Université Paris 13
Abstract:

In model checking, a well known source of state-space explosion (SSE) is the explicit representation of concurrent actions by their interleavings. Partial-order reductions (PORs) are a family of techniques attempting to cope with this by constructing an equivalent state space where irrelevant executions of the original are discarded.

This talk will be a gentle introduction to the topic. We will focus on Godefroid's persistent sets, prove that a selective exploration based on them visits all deadlocks, discuss the two main classes of algorithms for computing them, and finish, time permitting, with an overview of the conceptual similarities and differences between PORs and the unfolding technique.

Materials:
Table of contents, diamonds on the state space, relation to unfoldings, Godefroid's thesis, FG05, POPL'14.

Modèles et paradigmes de programmation parallèle distribuée

Date:
Oct. 30, 2014
Speaker:
Camille Coti, AOC, LIPN, Paris 13
Abstract:
Dans cette présentation, qui sera plus un panorama qu'un séminaire de recherche, je présenterai quelques grands paradigmes de programmation parallèle distribuée à travers les modèles de mémoire distribuée et de communications inter-processus. Le but de mon exposé sera de présenter comment le caractère distribué des données est représenté et manipulé dans ces paradigmes de programmation afin de réfléchir à quelles techniques de programmation adopter selon les patterns d'accès aux données d'un programme séquentiel que l'on souhaite paralléliser. Je mettrai l'accent sur la mémoire distribuée, la mémoire partagée distribuée, les sacs de tâches, les communications implicites unilatérales et bilatérales, la parallélisation automatique par compilation.
Materials:
Slides available here.

The implementation of GPGPU for Model Checking Problems

Date:
Oct. 23, 2014
Speaker:
Zhimin Wu, Nanyang Technological University, Singapore
Abstract:
In this presentation, I will introduce the implementation of GPGPU techniques in model checking area. I target Nvidia GPU so firstly, the latest CUDA Compute Architecture will be introduced, together with the key points of GPU Program optimization. Then I will refer to some existing research on GPU accelerated Model Checking Problems. Finally, I will briefly introduce my research work. (This will be an informal presentation.)
Materials:
Slides available in PDF. and PPT.

Unfolding-based Reachability Checking of Petri Nets

Date:
Oct. 9, 2014
Speaker:
César Rodríguez, LIPN, Université Paris 13
Abstract:

In model checking, a well known source of state-space explosion (SSE) is the explicit representation of concurrent actions by their interleavings. Partial-order reductions attempt to address this by constructing an equivalent state space where irrelevant executions of the original are discarded. A comparatively less well-known approach emerges from the use of partial-order semantics, where the state space is instead represented by a partial order where concurrent actions are simply left unordered. Petri net unfoldings are arguably the most prominent verification technique issued from this idea.

In this talk, three different semantics for Petri nets will be presented, the last one of which will be the aforementioned unfolding semantics. We will then see how unfoldings can be employed in practical verification and, time permitting, how to improve the method to address additional sources of SSE.

Materials:
Slides available here.