A language : Context Description Language (CDL)

CDL aims at formalizing the context with scenarios and temporal properties using property patterns. This DSML is based on UML 2. A CDL model describes, on the one hand, the context using activity and sequence diagrams and, on the other hand, the properties to be checked using property patterns. The originality of CDL is its ability to link each expressed property to a context diagram, i.e. a limited scope of the system behavior. allows contexts with scenarios and temporal properties using property patterns to be specified.

A toolset : Observer Based Prover (OBP)

OBP is an implementation of a CDL language translation in terms of formal languages. It takes as input a CDL model and generates a set of FIACRE programs after contexts splitting. OBP leverages existing academic simulators and model checkers, as TINA [LAAS] or OBP-Explorer [ENSTA-Bretagne].

fdf

Download OBP Explorer version 1.5.1

for Java 1.8, January 2018

Download OBP Explorer version 1.5.0

for Java 1.8, January 2017

Documentation

Examples (for OBP Explorer 1.4.5 and after)

for more examples, please contact us

Some publications

  • Valentin Besnard, Matthias Brun, Frédéric Jouault, Ciprian Teodorov, Philippe Dhaussy, Unified LTL Verification and Embedded Execution of UML Models, Models 2018 pdf

  • Vincent Leilde, Vincent Ribaud, Ciprian Teodorov, Philippe Dhaussy, A Problem-Oriented Framework to Diagnose Secured Applications, DETECT 2018 pdf

  • Vincent Leilde, Vincent Ribaud, Ciprian Teodorov, Philippe Dhaussy, Domain-oriented Verification Management, MEDI 2018 pdf

  • Fadi Obeid, Validation Formelle d’Implantation de Patrons de Sécurité, thèse de doctorat, Ensta Bretagne, UBL, juin 2018 pdf

  • Fadi Obeid et Philippe Dhaussy, Model-checking for Secured Component Implementation. SAM 2018 pdf

  • Fadi Obeid, Philippe Dhaussy, Validation Formelle d’Architectures Logicielles Basée sur des Patrons de Sécurité, AFADL'18 pdf

  • Vincent Leilde, Vincent Ribaud, Ciprian Teodorov, and Philippe Dhaussy, A diagnosis framework for critical systems verification, SEFM’17 pdf

  • Valentin Besnard, Matthias Brun, Philippe Dhaussy, Frédéric Jouault, David Olivier and Ciprian Teodorov. Towards one Model Interpreter for Both Design and Deployment. Conf EXE 2017 pdf

  • Lamia Allal, Ghalem Belalem, Philippe Dhaussy, Ciprian Teodorov. Using parallel and distributed reachability in model checking. RACCCS-2017 pdf

  • C. Teodorov, L. Le Roux, Z. Drey, and P. Dhaussy, “Past-Free[ze] reachability analysis: reaching further with DAG-directed exhaustive state-space analysis”, Software Testing, Verification and Reliability, Aug. 2016 pdf.

  • Vincent Leilde, Vincent Ribaud, Philippe Dhaussy, An Organizing System to Perform and Enable Verification and Diagnosis Activities, IDEAL’16. pdf

  • Vincent Leilde, Vincent Ribaud, Philippe Dhaussy, Model-based Diagnosis Patterns for Model Checking, PAME 2016 (co-located with MODELS’16). pdf

  • Ciprian Teodorov, Philippe Dhaussy, Luka Le Roux, Environment-driven Reachability for Timed Systems : Safety Verification of an Aircraft Landing Gear System, Int. Software Tools for Technology Transfer (STTT), DOI 10.1007/s10009-015-0401-2, Springer-Verlag, 2016 pdf.

  • Nadia Menad, Philippe Dhaussy, Zoé Drey, Rachida Mekki. Towards a Transformation Approach of Timed UML MARTE Specification for Observer-Based Verification. Computing and Informatics, to be published, 2016 pdf.

  • Vincent Ribaud, Ciprian Teodorov, Zoé Drey, Luka Le Roux and Philippe Dhaussy, Techniques and Challenges for Trace Processing from a Model-Checking Perspective. E-conference on Computer, Information, Systems Sciences, & Engineering (CISSE), 2014 pdf.

  • Teodorov C., Leroux L. and Dhaussy P. Context-aware Verification of a Cruise-Control System. 4th International Conference on Model & Data Engineering (MEDI), Larnaca, Cyprus, September 24-26, 2014. pdf

  • Philippe Dhaussy, Ciprian Teodorov, Context-aware Verification Technique to a Landing Gear System, 4th International ABZ 2014 Conference, Case Study Track, June 2 - 6 2014, Toulouse - France. pdf

  • L. Le Roux, J. Delatour et P. Dhaussy. Modélisation UML d'un régulateur de vitesse automobile. Revue Génie Logiciel, n° 109, Juin 2014 pdf (in french).

  • Jouault F., Téodorov C., Delatour J., Le Roux L. et Dhaussy P. Transformation de modèles UML vers Fiacre, via les langages intermédiaires tUML et ABCD. Revue Génie Logiciel, n° 109, Juin 2014 pdf (in french).

  • Dhaussy P., Le Roux L. et Téodorov C. Vérification formelle de propriétés : Application de l’outil OBP au cas d’étude CCS. Revue Génie Logiciel, n° 109, Juin 2014 pdf (in french).

  • L. Le Roux, P. Dhaussy et F. Boniol. Vérification formelle de propriétés basée sur une réduction de l'espace d'exploration de modèles. Revue Génie Logiciel, n° 107, décembre 2013 pdf (in french).

  • Nadia Menad, Philippe Dhaussy, A Transformation Approach for Multiform Time Requirements, 11th International Conference on Software Engineering and Formal Methods (SEFM’13), LNCS vol. 8137, September 25-27, pp. 16–30, 2013, Madrid, Spain pdf

  • Dhaussy P., Boniol F., Leroux L., Roger JC., Formal analysis of UML model, chapter in Modeling and Analysis of Embedded Systems, Whiley Editor. 2013 pdf.

  • Philippe Dhaussy, Frédéric Boniol, Jean-Charles Roger, and Luka Leroux, “Improving Model Checking with Context Modelling” Advances in Software Engineering, vol. 2012, Article ID 547157, 13 pages, 2012. doi:10.1155/2012/547157. See : http://www.hindawi.com/journals/ase/2012/547157/ or pdf

  • Philippe Dhaussy, Jean-Charles Roger, Luka Leroux, Frédéric Boniol, Context Aware Model Exploration with OBP tool to Improve Model-Checking. ERTS’12, febuary 1-3, 2012. paper (pdf) talk (pdf)

  • Amine Raji, Intération des actvités de preuve dans le processus de développement de logiciels pour les systèmes embarqués. Thèse de doctorat, Ensta Bretagne - Telecom Bretagne, LabSticc, mars 2012 pdf

  • Philippe Dhaussy, Frédéric Boniol, Jean-Charles Roger, Reducing State Explosion with Context Modeling for Model-Checking. 13th IEEE International High Assurance Systems Engineering Symposium (Hase’11), Boca Raton, USA. November 10-12, 2011. pdf

  • Xavier Dumas, Frédéric Boniol, Philippe Dhaussy, Eric Bonnafous, Application of partial-order methods for the verification of closed-loop SDL systems, ACM Symposium On Applied Computing (SAC’11), TaiChung, Taiwan, March 2011. pdf

  • Amine Raji, Philippe Dhaussy, Bruno Aizier, Automating Context Description for Software Formal Verification, Workshop MoDeVVa 2010, Oslo, Norway, October 4th 2010. pdf

  • Amine Raji, Philippe Dhaussy, User Context Models : A framework to ease software formal verifications,12th International Conference on Enterprise Information Systems (ICEIS’10), 8-12 june, 2010, Funchal, Madeira. pdf

  • Xavier Dumas, Frédéric Boniol, Philippe Dhaussy, Eric Bonnafous, Context Modelling and Partial-Order Reduction: Application to SDL Industrial Embedded Systems, IEEE Symposium on Industrial Embedded Systems (SIES’10), Trento, Italy, July 7-9, 2010. pdf

  • Dhaussy P., Pierre-Yves Pillain PY., Creff S., Raji A., Le Traon Y., Baudry B. Contribution à la formalisation de contextes et d’exigences pour la validation formelle de logiciels embarqués. Conférence Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL’10), Poitiers-Futuroscope, 09-11 Juin 2010. pdf (in french)

  • Dhaussy P., Pierre-Yves Pillain PY., Creff S., Raji A., Le Traon Y., Baudry B. Evaluating Context Descriptions and Property Definition Patterns for Software Formal Validation. In Lecture Notes in Computer Science 5795, Springer Verlag, Andy Schuerr, Bran Selic (Eds): 12th IEEE/ACM conf. Model Driven Engineering Languages and Systems (Models’09), No 5795 (2009), pages 438-452. paper pdf talk pdf

  • Xavier Dumas, Frédéric Boniol, Philippe Dhaussy, Eric Bonnafous. Context Constraints Method for Software Formal Verification. ESA Workshop on Avionics Data, Control and Software Systems (ADCSS), Noordwijk, The Netherlands, 3-5 November 2009.

  • Ph.Dhaussy, J.Auvray, S.De Belloy, F.Boniol, E. Landel, Un langage de contexte de preuve pour la validation formelle de modèles logiciels, Conférences LMO’08 et CAL’08, Montréal, 3 au 7 mars 2008. Revue RNTI L-2. pdf (in french)

  • A. Monégier du Sorbier, S. de Belloy, F. Turpin, Ph. Dhaussy, Expérimentation de composants de preuve pour le développement de composants logiciels embarqués, Journées NEPTUNE'2008, Paris, 8-9 avril 2008, Revue Génie logiciel, juin 08, N° 85. pdf (in french)

  • Ph.Dhaussy, F.Boniol, Mise en oeuvre de composants MDA pour la validation formelle de modèles de systèmes d’information embarqués, revue RSTI- ISI, Vol. 12, N° 5/2007, pages 133-157. pdf (in french)