User Tools

Site Tools


home

A language : Context Description Language (CDL)

A toolset : Observer Based Prover (OBP)

Bookmark and Share

Contact : Philippe Dhaussy ENSTA-Bretagne Lab. STICC UMR CNRS 6285 philippe.dhaussy at ensta-bretagne.fr

A DSL "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].

cdl_transfo_with_obp.jpg

Download OBP Explorer version 1.5.0 (for Java 1.8, January 2017)

Download OBP Explorer version 1.4.9 (for Java 1.8, January 2016)

Download Documentation

Download examples (for OBP Explorer 1.4.5 and after)

Some publications

  • 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.
  • 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)
home.txt · Last modified: 2017/01/20 13:48 by dhaussph