Test case selection in model-based testing is discussed in [CMO09], focusing on the use of a similarity function. Automatically generated test suites usually have redundant test cases. The reason is that test generation algorithms are usually based on structural coverage criteria that are applied exhaustively. These criteria may not be helpful to detect redundant test cases as well as the suites are usually impractical due to the huge number of test cases that can be generated. Both problems are addressed by applying a similarity function.
The work presented in [DFM09] proposes a strategy and an algorithm for generating abstractions of systems modeled in the process algebra CSP. These abstractions are safe in the sense that they preserve trace-based refinements. Also, a strategy and a framework to evaluate functional testing techniques is presented in [BM09]. The framework is defined compositionally and parametrically. This allows us to characterize different aspects of systems in an incremental way as well as test specific hypothesis about the system under test.
Finally, a testing theory, based on the CSP process algebra, whose conformance relation (cspio) distinguishes input and output events is presented in [SNM09]. Although cspio has been defined in terms of the standard CSP traces model, we show that our theory can be immediately extended to address deadlock, outputlock and livelock situations if a special output event is used to represent quiescence. This is formally established by showing that this broader view of cspio is equivalent to Tretmans' ioco relation.
Results by the French team:
In [BBBB09], we propose an abstract procedure which, given a timed automaton, produces a language-equivalent deterministic infinite timed tree. We prove that under a certain boundedness condition, the infinite timed tree can be reduced into a classical deterministic timed automaton. The boundedness condition is satisfied by several subclasses of timed automata, some of them were known to be determinizable (event-clock timed automata, automata with integer resets), but some others were not. We prove for instance that strongly non-Zeno timed automata can be determinized. As a corollary of those constructions, we get for those classes the decidability of the universality and of the inclusion problems, and compute their complexities (the inclusion problem is for instance EXPSPACE-complete for strongly non-Zeno timed automata). During 2010, we expect to use this determinisation procedure for test generation from non-deterministic timed automata.
In the application domain of component-based system design, developing theories which support compositional reasoning is notoriously challenging. In [BPR09], we define timed modal specifications, an automata-based formalism combining modal and timed aspects. As a stepping stone to compositional approaches of timed systems, we define the notions of refinement and consistency, and establish their decidability. This work can serve as a basis for further common work about compositional testing.
In [MDJ09a], we investigate the combination of controller synthesis and test generation techniques for the testing of open, partially observable systems with respect to security policies. We consider two kinds of properties: integrity properties and cofidentiality properties. We assume that the behavior of the system is modeled by a labeled transition system and assume the existence of a black-box implementation. We first outline a method allowing to automatically compute an ideal access controls ensuring these two kinds of properties. Then, we show how to derive testers that test both the conformance of the implementation with respect to its specification, the correctness of the real access control that has been composed with the implementation in order to ensure a security property, and the security property itself.
In the application domain of component-based system design, developing theories which support compositional reasoning is notoriously challenging. In [BPR09], we define timed modal specifications, an automata-based formalism combining modal and timed aspects. As a stepping stone to compositional approaches of timed systems, we define the notions of refinement and consistency, and establish their decidability. This work can serve as a basis for further common work about compositional testing.
In [MDJ09a], we investigate the combination of controller synthesis and test generation techniques for the testing of open, partially observable systems with respect to security policies. We consider two kinds of properties: integrity properties and cofidentiality properties. We assume that the behavior of the system is modeled by a labeled transition system and assume the existence of a black-box implementation. We first outline a method allowing to automatically compute an ideal access controls ensuring these two kinds of properties. Then, we show how to derive testers that test both the conformance of the implementation with respect to its specification, the correctness of the real access control that has been composed with the implementation in order to ensure a security property, and the security property itself.
Visit of Sidney Nogueira
During his visit in Rennes Sidney Nogueira gave two talks about his current work with Augusto Sampaio.
The first talk was about the conformance relation cspio, which distinguishes
input and output events, based on the CSP process algebra. This
relation has been adopted in an industrial context involving a
collaboration with Motorola, whose focus is on the testing of mobile
applications. Although cspio has been defined in terms of the
standard CSP traces model, we show it can be immediately extended to
address deadlock, outputlock and livelock situations, if a special
output event is used to represent quiescence. This is formally
established by showing that the broader view of cspio can be is
equivalent to Tretmans' cspio relation. Furthermore, we talk about
possible compositionality properties for cspio with respect to several
CSP operators. This talk is the basis of an invited talk given by Augusto Sampaio at ICFEM'09.
Discussions with Sidney Nogueira followed concerning compositional
test case generation: how to generate test cases from composed specifications
in a modular way.
The second talk was about
enhancements applied in a use case
template used to describe behavior of mobile phone applications to be
tested; what is motivated by the context of the Brazilian Test Center
project. The enhancements regard the possibility to specify use case
relations from UML in addition to the definition of individual use
cases, which are composed of interconnected flows. Moreover, this
modified template enables the definition and manipulation of data, and
the communication of inputs and outputs. In the sequel, the
translation of the use cases to its formal representation as CSP
processes. Finally, we show how CSP test purposes can specify test
scenarios that match a particular specification state, and how test
scenarios that match a test purpose can be obtained as counter
examples of a refinement checking between processes.
Visit of N. Bertrand, H. Marchand and T. Jéron in Brazil
In december 2009, we plan to visit the Brasilian team before and during the ICFEM'09 conference in Rio. Several researchers of both teams are involved in the conference as PC members (P. Machado, T. Jéron), authors (N. Bertrand) and invited speaker (Augusto Sampaio). This is thus a good oportunity to meet in Brazil. The schedule is not yet decided but meetings will take place in Rio and/or Recife.
Publications in 2009
[AMAA09] Andrade, Wilkerson de Lucena ; Machado, P. D. L. ; Alves,
Everton ; Almeida, Diego Rodrigues. Test Case Generation of Embedded
Real-Time Systems with Interruptions for FreeRTOS. In: Brazilian
Symposium on Formal Methods, 2009, Gramado. SBMF 2009 - Brazilian
Symposium on Formal Methods, 2009. p. 54-69. To be published in the
LNCS series by Springer.
[AM09] Andrade, Wilkerson de Lucena ; Machado, P. D. L. . Interruption Testing of Reactive Systems. In: Brazilian Symposium on Formal Methods, 2009, Gramado. SBMF 2009 - Brazilian Symposium on Formal Methods, 2009. p. 37-53. To be published in the LNCS series by Springer. (invited paper)
[CMO09] Cartaxo, Emanuela G. ; Machado, P. D. L. ; Oliveira Neto, Francisco G.. On the use of a similarity function for test case selection in the context of model-based testing. Software Testing, Verification and Reliability, 2009. DOI 10.1002/stvr.413. (Early view in advance of print).
[DFM09] Damasceno, Adriana Carla ; Farias, Adalberto ; Mota, A. . A Mechanized Strategy for Safe Abstraction of CSP Speci cations. In: Simpósio Brasileiro de Métodos Formais, 2009, Gramado. Brazilian Symposium on Formal Methods (SBMF 2009), 2009. v. 12. p. 118-133.
[BM09] Bertolini, Cristiano ; Mota, A. . Using Probabilistic Model Checking to Evaluate GUI Testing Techniques (aceito p publicação). In: Software Engineering and Formal Methods, 2009, Hanoi. 7th IEEE International Conference on Software Engineering and Formal Methods, 2009.
[SNM09] Sampaio, A. C. A.; Nogueira, Sidney; Mota, Alexandre. Compositional Verification of Input Output Conformance via CSP Refinement Checking. In: ICFEM - International Conference on Formal Engineering Methods, 2009, Rio de Janeiro. International Conference on Formal Engineering Methods. Berlin : Springer Verlag - Lecture Notes in Computer Science, 2009. (invited paper)
[BBBB09] C. Baier, N. Bertrand, P. Bouyer, Th. Brihaye, When are timed automata determinizable?, in 36th International Colloquium on Automata, Languages and Programming (ICALP'09), LNCS No 5556, Pages 43-54, Rhodes, Greece, July 2009.
[BPR09] N. Bertrand, S. Pinchinat, J.B. Raclet, Refinement and Consistency of Timed Modal Specifications, in Proceedings of the 3rd International Conference on Language and Automata Theory and Applications (LATA'09), LNCS No 5457, Pages 152-163, Tarragona, Spain, April 2009.
[MDJ09a] H. Marchand, J. Dubreil, T. Jéron, Automatic Testing of Access Control for Security Properties, in TestCom'09, 2009.
[MDJ09b] H. Marchand, J. Dubreil, T. Jéron, Génération automatique de tests pour des propriétés de sécurité, in 4ème Conférence sur la Sécurité des Architectures Réseaux et des Systèmes d'Information, Pages 157-174, June 2009.
[J09] T Jéron, Génération de tests pour les systèmes réactifs et temporisés, Actes de l'Ecole d'Eté Temps-Réel, Télécom ParisTech, Paris, September 2009.
(1) DR / CR / professeur
(1) post-doc / doctorant / stagiaire
[AM09] Andrade, Wilkerson de Lucena ; Machado, P. D. L. . Interruption Testing of Reactive Systems. In: Brazilian Symposium on Formal Methods, 2009, Gramado. SBMF 2009 - Brazilian Symposium on Formal Methods, 2009. p. 37-53. To be published in the LNCS series by Springer. (invited paper)
[CMO09] Cartaxo, Emanuela G. ; Machado, P. D. L. ; Oliveira Neto, Francisco G.. On the use of a similarity function for test case selection in the context of model-based testing. Software Testing, Verification and Reliability, 2009. DOI 10.1002/stvr.413. (Early view in advance of print).
[DFM09] Damasceno, Adriana Carla ; Farias, Adalberto ; Mota, A. . A Mechanized Strategy for Safe Abstraction of CSP Speci cations. In: Simpósio Brasileiro de Métodos Formais, 2009, Gramado. Brazilian Symposium on Formal Methods (SBMF 2009), 2009. v. 12. p. 118-133.
[BM09] Bertolini, Cristiano ; Mota, A. . Using Probabilistic Model Checking to Evaluate GUI Testing Techniques (aceito p publicação). In: Software Engineering and Formal Methods, 2009, Hanoi. 7th IEEE International Conference on Software Engineering and Formal Methods, 2009.
[SNM09] Sampaio, A. C. A.; Nogueira, Sidney; Mota, Alexandre. Compositional Verification of Input Output Conformance via CSP Refinement Checking. In: ICFEM - International Conference on Formal Engineering Methods, 2009, Rio de Janeiro. International Conference on Formal Engineering Methods. Berlin : Springer Verlag - Lecture Notes in Computer Science, 2009. (invited paper)
[BBBB09] C. Baier, N. Bertrand, P. Bouyer, Th. Brihaye, When are timed automata determinizable?, in 36th International Colloquium on Automata, Languages and Programming (ICALP'09), LNCS No 5556, Pages 43-54, Rhodes, Greece, July 2009.
[BPR09] N. Bertrand, S. Pinchinat, J.B. Raclet, Refinement and Consistency of Timed Modal Specifications, in Proceedings of the 3rd International Conference on Language and Automata Theory and Applications (LATA'09), LNCS No 5457, Pages 152-163, Tarragona, Spain, April 2009.
[MDJ09a] H. Marchand, J. Dubreil, T. Jéron, Automatic Testing of Access Control for Security Properties, in TestCom'09, 2009.
[MDJ09b] H. Marchand, J. Dubreil, T. Jéron, Génération automatique de tests pour des propriétés de sécurité, in 4ème Conférence sur la Sécurité des Architectures Réseaux et des Systèmes d'Information, Pages 157-174, June 2009.
[J09] T Jéron, Génération de tests pour les systèmes réactifs et temporisés, Actes de l'Ecole d'Eté Temps-Réel, Télécom ParisTech, Paris, September 2009.
Rapport financier 2009
Avant de remplir les tableaux, consultez les règles au paragraphe "Financement" de la page d'accueil du programme.
| 1. Dépenses EA (effectuées sur les crédits de l'Equipe Associée) | Montant dépensé |
| Invitations des partenaires | 2330&euro |
| Missions INRIA | ~ 7140&euro |
Total | 9470&euro |
Justifiez en quelques lignes l'utilisation des crédits et en particulier une utilisation partielle du budget alloué.
Le budget 2009 est encore approximatif, puisque nous prévoyons une visite de 3 personnes au Brésil en décembre 2009. Nous estimons le coût de ces missions à: voyage: 1500 &euro x 3 = 4500 &euro, séjour: 110 &euro /j x 8j x 3 pers = 2640 &euro, soit au total 7140 &euro. Nous sommes de toutes façons en deça du budget alloué. Pour plusieurs raisons (voir plus haut) les visites Brésil vers France ont été peu nombreuses cette année.| 2. Dépenses externes (effectuées sur des financements hors EA) | Montant dépensé | |
| Nom de l'organisme 1 (*): | ||
| Invitations des partenaires | ||
| Missions INRIA vers le partenaire | ||
Total | ||
| Nom de l'organisme 2 (*): | ||
| Invitations des partenaires | ||
| Missions INRIA vers le partenaire | ||
Total | ||
(*) Ajouter ou supprimer des lignes au tableau ci-dessus
de façon à faire figurer tous les organismes ayant contribué au financement
de l'équipe associée
Total des financements externes dépensés |
Total des financements EA et externes dépensés |
~ 9470&euro |
Bilan des échanges effectués en 2009
1. Chercheurs Seniors
Nom |
statut (1) |
provenance | destination |
objet (2) |
durée (3) |
Coût (si financement EA) |
Coût (si financement externe) |
| Bertrand Nathalie | CR Inria | Rennes | Brésil | Visite | 1 semaine | 2380&euro | |
| Jéron Thierry | DR Inria | Rennes | Brésil | Visite | 1 semaine | 2380&euro | |
| Marchand Hervé | DR Inria | Rennes | Brésil | Visite | 1 semaine | 2380&euro | |
Total des durées |
3 semaines |
(1) DR / CR / professeur
(2) colloque, thèse, stage, visite....
(3) précisez l'unité (mois, semaine..)
2. Juniors
Nom |
statut (1) |
provenance |
destination | objet (2) |
durée (3) |
Coût (si financement EA) |
Coût (si financement externe) |
| Sidney de Carvalho Nogueira | PhD student | Brésil | Rennes | Visite | 1 semaine | 2330&euro | |
Total des durées |
1 semaine |
(1) post-doc / doctorant / stagiaire
(2) colloque, thèse, stage, visite....
(3) précisez l'unité (mois, semaine..)
III. PREVISIONS 2010
Programme de travail
Description du programme scientifique de travail pour l'année 2010Work Breakdown
The work program for 2010 will be a continuation and a precision of the program for 2009
(see http://www.irisa.fr/vertecs/EA-Brazil09.html ).
We recall that we wish to cooperate at four levels:
- Fundamental Background. This consists in investigating and developing theoretical background that supports the main techniques and tools to be developed as part of the goal. For this cooperation, this is mainly related to test models and their semantics (LTS, IOLTS, IOSTS, Timed automata), algorithms for test generation, as well as their relationship to the conformance relations (e.g. ioco for LTS models, tioco for timed models, and variants).
- Process Development. Methods, strategies and processes are going to be developed to support the practical application of the goal. For this project, this is mainly related to test case generation, selection and abstraction methods and strategies along with practical processes where they can be applied. We also want to study the relations between testing and other validation techniques such as verification, diagnosis, control synthesis, monitoring.
- Tools Development. Tools that support the main methods and strategies defined are going to be designed and/or prototyped. We expect that these tools will interoperate with tools already developed by the teams such as TGV/STG and Target.
- Experimentation and Validation.
At this step, case
studies are going to be conducted to improve and/or validate the
solutions proposed. Two main domains are going to be considered:
- Control-command systems. Control-command systems are present in several application domains such as transport and energy. Systems in this domain share a lot of features: these are critical systems communicating with their external environment (human, software or hardware), they command and/or observe other systems (security management, activators, etc). They manipulate a great amount of heterogenous data (boolean values, integers, reals) and must react in real-time. Due to their critical nature, their correct functioning is crucial. They should thus be heavily verified and tested. Advances in model-based testing, in particular increasing the coverage of test suites while not dramatically increasing its size is thus crucial in these domains. These systems are thus well targeted by the research we intend to conduct in this project. It is also the target of the French RNTL Testec project started in 2008.
- Mobile phone applications. This domain is characterized by applications, composed of a number of features, that are highly interactive, having their flow of execution guided mostly by external input. These applications are often tested manually. Also, the gap between specification and program is narrow, since the logics are captured by external interactions. In this context, feature testing (FT) is a crucial testing activity. A feature is a set of individual requirements that describes some functionality. Alarm Clock, Phonebook and Messaging are example of features usually found in mobile phone applications. A functional understanding of these applications is more effectively achieved by investigating user interface tasks behaviour. Features can interrupt the flow of execution of other features at any time. The possible number of combinations of allowed interruptions at different points of a flow of execution is huge. This makes the specification of each possibility unfeasible by using conventional notations and strategies. As a consequence and also due to the lack of a suitable test model, test case generation and selection is compromised.
Expected Results
Below is a list of expected results according to the main goals
presented in the objectives, some of which being already started (see the results for 2009 above) :
- Interruption testing.
- A test model for interruption testing that is capable of modelling features and their interruptions;
- Experimentation and validation of test case generation and selection strategies.
- More powerful models and properties.
- Test models and theories as well as test generation techniques for systems with heterogenous features. In particular timed models are investigated on both sides, and in particular problems linked to partial observation and non-determinism for this model. In the continuation of previous work carried on pushdown models for the modelisation of systems with recursion, we will try to extend our results to graph grammars.
- Abstract interpretation of test cases.
- A method of discovering defects automatically by applying model checking and testing together;
- A method to derive high-level properties into low-level properties;
- Abstraction techniques to incorporate model checking and testing in the same software process development.
- Testing and learning.
- Theroretical and methodological results on the combination of testing and learning.
- Test case generation from process algebraic models.
- Definition of an implementation relation in terms of CSP that generates test cases capable to observe the failures and divergences of the implementation under test during the testing;
- A systematic approach that uses the domain specific requirements embedded in CSP specifications for the purpose of test generation.
- Improved coverage-based test selection.
- Formal characterization of semantic-based coverage criteria and corresponding coverage-based test selection algorithms.
- Test case selection based on a similarity function.
- Test case selection techniques for model-based testing that cope with redundancy for minimizing test suites;
- Experimental studies on test case selection for embedded systems.
- Testing security aspects.
- We already had some results on testing of information flow and integrity, based on a combination of diagnosis and control synthesis. We want to continue in this direction and explore different properties such as availability
- We also want to explore the relations with monitoring of security properties in a partial observation setting.
Methodology
The project is going to be conducted by cooperation of Brazilian and French
team members. However, each team will be responsible for specific
goals defined in the objective section. There is a general
coordinator at each side. Each coordinator will assign tasks to
the researchers involved and his team of PhD and MSc Students
and Research Assistants. In addition, we expect that PhD students
can be co-supervised by researchers in both teams.
Each task is going to be planned in terms of the intended scope, milestones and expected results according to the global plan for the project. Also, task results are going to be documented in technical reports and communicated among team members.
There are going to be periodical meetings by Internet conference call where team members can present short seminars for exchanging ideas and receiving feedback. Visits from team members are also planned for closer discussions and for checking results. We plan to have 2 workshops, one in Brazil and one in France, as forums to present, check and disseminate results produced by the cooperation.
Results and milestones are going to checked and evaluated at the end of each 6 months. The goal is to assess progress and adjust and update initial plan and objectives.
Finally, the group will use a common repository of discussions and documents related to the cooperation as well as a discussion list.
Each task is going to be planned in terms of the intended scope, milestones and expected results according to the global plan for the project. Also, task results are going to be documented in technical reports and communicated among team members.
There are going to be periodical meetings by Internet conference call where team members can present short seminars for exchanging ideas and receiving feedback. Visits from team members are also planned for closer discussions and for checking results. We plan to have 2 workshops, one in Brazil and one in France, as forums to present, check and disseminate results produced by the cooperation.
Results and milestones are going to checked and evaluated at the end of each 6 months. The goal is to assess progress and adjust and update initial plan and objectives.
Finally, the group will use a common repository of discussions and documents related to the cooperation as well as a discussion list.
Programme d'échanges avec budget prévisionnel
1. Echanges
Décrivez
les échanges prévus dans les deux sens : invitations de chercheurs de votre
partenaire et missions INRIA vers votre partenaire ;
Précisez s'il
s'agit de chercheurs confirmés ou de juniors (stagiaires, doctorants,
post-doctorants) ;
Motivez,
si possible, les raisons scientifiques (travail commun, workshop,..) et
précisez la durée prévue ;
Indiquez
les étudiants impliqués dans la proposition. Donnez une estimation
de leur nombre, pour chaque partenaire, et précisez si des thèses
en cotutelle sont prévues ;
Résumez
ensuite ces informations dans les tableaux 1 et 2 ci-dessous en faisant une
estimation budgétaire :
| 1. ESTIMATION DES DÉPENSES EN MISSIONS INRIA VERS LE PARTENAIRE | Nombre de personnes
|
Coût estimé
|
| Chercheurs confirmés | 2 | 4000&euro |
| Post-doctorants |
||
| Doctorants | 2 | 6000&euro |
Stagiaires |
||
| Autre (précisez) : |
||
Total
|
10 000&euro |
| 2. ESTIMATION DES DÉPENSES EN INVITATIONS DES PARTENAIRES | Nombre de personnes
|
Coût estimé
|
| Chercheurs confirmés | 2 | 4000&euro |
| Post-doctorants |
||
| Doctorants | 2 | 6000&euro |
Stagiaires |
||
| Autre (précisez) : |
||
Total
|
10 000&euro |
2. Cofinancement
Cette coopération bénéficie-t-elle déjà d'un
soutien financier de la part de l'INRIA, de l'organisme étranger partenaire
ou d'un organisme tiers (projet européen, NSF, ...) ?
Indiquez ces éléments et donnez les montants associés.
About funding for the cooperation from the brazilian part, we have
some that support scholarships for students and travel funding for
attending events. This year there was no opportunity for applying to
international cooperation. However, there is an open one for 2010.
3. Demande budgétaire
Indiquez, dans le tableau ci-dessous, le coût global estimé de
la proposition et le budget demandé à la DRI dans le cadre de
cette Equipe Associée.
(maximum
20 K€ pour une prolongation en 2e année et 10 K€ pour une
3e année).
Commentaires
|
Montant
|
| A. Coût global de la proposition (total des tableaux 1 et 2 : invitations, missions, ...) | 20 000&euro |
| B. Cofinancements utilisés (financements autres que Equipe Associée) | |
Financement "Équipe Associée" demandé (A.-B.) |
Remarques ou observations :
© INRIA - mise à jour le 08/07/2009