hal-00015031, version 1

Test of object-based specifications using B notations

Ninh Thuan Truong () ¹, Jeanine Souquières ¹

(2005)

• 1:  DEDALE (LORIA)
• 
  INRIA – CNRS : UMR7503 – Université Henri Poincaré - Nancy I – Université Nancy II – Institut National Polytechnique de Lorraine (INPL) France

Bibliographic reference

• Type of document: Documents without publication reference (Preprint)
• Subject: Computer Science/Mathematical Software
• Title: Test of object-based specifications using B notations
• Abstract: We propose an approach to test object-based specifications using B notations. We start from an UML specification in the form of a class diagram and sequence diagrams which express scenarios modelling the system's behavior. These diagrams are transformed into a B specification which is completed by the definition of the operations (messages in the sequence diagrams corresponding to the methods in the class diagram), and safety and dynamic properties on the system. The test of scenarios and the satisfaction of the properties is done by means of a theorem prover.
• Fulltext language: English
• Production date: 2005

Attached file list to this document: 

• hal-00015031, version 1
• http://hal.archives-ouvertes.fr/hal-00015031
• oai:hal.archives-ouvertes.fr:hal-00015031
• From: Ninh Thuan Truong <>
• Submitted on: Friday, 2 December 2005 09:41:43
• Updated on: Friday, 11 May 2007 18:59:55