CITI has stopped operations in 2014, to co-launch NOVA LINCS THIS SITE IS NOT BEING UPDATED SINCE 2013
citi banner
Home Page FCT/UNL UNL
  Home  \  Seminars @ CITI  \  Seminar Page Login  
   
banner bottom
File Top
SATEL: How to express test intentions
{ Wed, 27 Jun 2007, 10h00 }

By: Didier Buchs  [ show info ]

talk is devoted to the presentation of an integrated framework for modeling, implementing and verifying systems with a maximum confidence in the resulting critical system. We will present a semi-automatic approach to test generation which is materialized in the test intention language SATEL (Semi-Automatic Testing Language) for CO-OPN (Concurrent Object Oriented Petri Nets). The approach is semi-automatic in the sense that we allow the test engineer to state test purposes (which we call in our approach test intentions), while using unfolding techniques (introduced by Bernot, Gaudel and Marre) for automatically finding equivalence classes of inputs to operations of the model. While designing the test language it was our intention to explicitly make use of the test engineer's knowledge in the test generation process. He/she is able to express which parts of the model are relevant for testing and to impose limits on how that testing should be performed. With SATEL we have tried to devise a test generation framework that automates the typical approach of a test engineer rather than performing an exhaustive search of the model. The semi-automatic aspect SATEL corresponds to the fact that, given an operation of the model (from a black-box perspective), the test engineer will be also be able to state that the generated tests should include inputs that automatically cover the various behaviors (also called in the literature equivalence classes) of that operation. The test intentions in SATEL correspond to generalizations of the behavior of the SUT and are expressed by writing execution patterns with variables over sequences of input/output events of the specification --- one could also see them as testing macros. The instantiation of these variables by the test language compiler will yield test cases for the specified test intentions. We have also included in SATEL support for non-determinism at two levels. Firstly the formalism in which we express our tests is the HML (Hennessy-Milner logic) which is a branching temporal logic. In this way we are able to express tests which reflect non- deterministism both at the level of the specification and of the SUT. Secondly we have included in our language a means of treating a specific kind of non-determinism of the SUT while it is interacting with the environment. This is done by anticipating a reply (a stimulation) to a given non-deterministic observation by means of a predefined function at the level of the specification. SATEL has been implemented in our framework CoopnBuilder environment and we are currently validating our approach by applying it to an industrial case study.


Hosted by: Software Systems

Location: Sala de SeminĂ¡rios do CITI

File Bottom