-
KEDGEN2: A key establishment and derivation protocol for EPC Gen2 RFID systems
International audience -
Model Checking using Generalized Testing Automata
International audience -
Formal Analysis of the ACE Specification for Cache Coherent Systems-on-Chip
International audience -
CAESAR_SOLVE: A Generic Library for On-the-Fly Resolution of Alternation-Free...
Boolean Equation Systems (BESs) provide a useful framework for modeling various verification problems on finite-state concurrent systems, such as equivalence checking... -
Analyse à partir du modèle
Les systèmes embarqués rendent un nombre de services grandissant et font partie de notre vie quotidienne : ascenseurs, transports, téléphonie, médecine énergie,... -
Formal modelling and analysis of behaviour grading within a peer-to-peer stor...
International audience -
ScaleSem : model checking and semantic web
The increasing development of networks and especially the Internet has greatly expanded the gap between heterogeneous information systems. In a review of studies of... -
Decentralized diagnosis and diagnosability by model checking
International audience -
IDM pour une approche combinant synthèse et vérification de modèles
International audience -
Modélisation et analyse de systèmes asynchrones avec CADP
La conception des systèmes industriels critiques comportant du parallélisme asynchrone nécessite l'utilisation de méthodes formelles, assistées par des outils de... -
Extending Symmetry Reduction Techniques to a Realistic Model of Computation
Much of the literature on symmetry reductions for model checking assumes a simple model of computation where the local state of each component in a concurrent system... -
Formal Verification of Concurrent Systems via Directed Model Checking
Model checking suffers from the state explosion problem, due to the exponential increase in the size of a finite state model as the number of system components grows.... -
Automatic Verification of Bossa Scheduler Properties
Bossa is a development environment for operating-system process schedulers that provides numerous safety guarantees. In this paper, we show how to automate the... -
On the Decidability of the Safety Problem for Access Control Policies
An access control system regulates the rights of users to gain access to resources in accordance with a specified policy. The rules in this policy may interact in a... -
Assumption-Commitment Support for CSP Model Checking
We present a simple formulation of Assumption-Commitment reasoning using CSP. In our formulation, an assumption-commitment style property of a process SYS takes the... -
A Transformation Approach for Multiform Time Requirements
International audience -
Model-checking Distributed Components: The Vercors Platform
This article presents a component verification platform called Vercors providing means to analyse the behaviour properties of applications built from distributed... -
Simulation and Verification of UML-based Railway Interlocking Designs
The development of safety critical systems such as railway interlocking systems demands the application of formal methods in order to verify the operativeness and the... -
Towards Timed Business Process View Generation
International audience -
Elements Of Epistemic Crypto Logic
The talk presents an extension of DEL (dynamic epistemic logic) intended for model checking of cryptographic protocols. Key elements are a feasible epistemic...
