There are many teams working on testing worldwide. Our proposal
lies in the model-based testing community (see e.g. [
] for a recent overview), where the core events are Testcom and Fates conferences.
More precisely, we found our work on the
]. Initial works with similar models
were based on enumerative techniques (Brinksma (Twente) and
Tretmans (Nijmegen) developing TorX, Jonsson (Uppsala),
Grieskamp-Schulte (FSE Microsoft, Spec Explorer), Cleaveland
(Reactive Systems, inc, Reactis Tester)). The originality of the
TGV approach the French Team took with Verimag
[
], was to design efficient test selection
algorithms using on-the-fly model-checking techniques, avoiding
the exploration of the complete state space. The Brazilian team
has developed on this approach by exploring model checking
techniques for test purpose generation [
].
Moreover, the brazilian team focusses on testing of interruptions in concurrent systems.
This is also based on the ioco-theory and on the use of the TGV
tool as well as symbolic approaches. As related work, Lorentsen
[
] proposes the use of colored Petri nets for modelling
interactions from which test cases can be derived. Furthermore,
approaches that capture domain specific requirements while using
model-based testing are being developed. The HoTTest tool
[
] uses a strongly typed domain-specific
language to model the system under test that enables the automatic
extraction and embeds domain specific requirements into the test
models. In addition, the Archetest tool [
] performs
several model transformations that lead to a test model that
exposes domain specific information.
More recently test selection techniques have been designed on
models with both control and data. For these models, some
approaches are based on symbolic execution, combined with
constraint solving (Gaudel (Orsay), Le Gall-Gaston (Evry - CEA,
Agatha), Marre (CEA, Gatel), Legeard (Inria Cassis, BZ-Testing
Tool), Peled-Gunter (U. Warwick, PET)), with random exploration
(Godefroid (ex-Bell, DART)).
Some other approaches are based on abstractions,
combined with TGV (Van de Pol (CWI)),
or based on predicate abstraction, reachability analysis and
symbolic execution (Ball (Microsoft)). The originality of the work
carried on by the French team is to deal with non-determinism
(most works are limited to deterministic models), to generate test
programs (almost all others produce instantiated test cases), and
to use abstract interpretation (to our knowledge, none of the
others do). There are several groups working on test selection on
timed models (Tripakis (ex-Verimag), Brinksma (Twente),
Larsen (Aalborg, T-Uppaal)). On the other hand, the Brazilian team
has investigated on test selection in the context of embedded
systems by considering semantical criteria. This is innovative in
the sense that, for functional testing, test selection strategies
currently proposed are mostly based on structural criteria and
probabilistic models [
].
In this cooperation, we expect to mix symbolic techniques for
models with both time, interruption and data. We are not aware of
any other group trying to deal with recursion in test case
selection.
] proposed an approach combining model
checking and testing: black box checking. Their approach tests
whether an implementation satisfies some given properties. It
assumes that the structure of the implementation is unknown and
there is incomplete information to perform model checking
directly. Thus, the specification model is adjusted using a
learning approach based on Angluin's algorithm. A variation of the
black box checking is the Adaptive model checking [
].
This approach considers an incorrect but not obsolete model and
explores it by learning the incorrect model to construct the
correct model by adapting black box testing and machine learning
techniques together. The works in
[
]
use dynamic analysis in order
to check properties into the system. In these approaches, the
system is analyzed dynamically by its execution, and invariants,
pre and post-conditions are obtained automatically. Also, new
software model checkers have been used by the industry in which
properties are checked directly in the system without the use of
explicit models [
].
We are investigating how high-level properties can be derived
automatically in low-level properties by integrating test case
generation and model checking techniques.
[
BJK*05] M. Broy, B. Jonsson, J.-P. Katoen, M. Leucker, and A. Pretschner, editors.
Model-based testing of reactive systems: advanced lectures , volume 3472 of LNCS. Springer-Vermag, 2005.
[
CJRZ02] D. Clarke, T. Jéron, V. Rusu, and E. Zinovieva. Stg: A symbolic test generation tool.
In TACAS'02: Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems , pages 470-475, London, UK, 2002. Springer-Verlag.
[
CJJ07] C. Constant, B. Jeannet, and T. Jéron. Automatic test generation from interprocedural specifications.
In TestCom/Fates07 , LNCS, Tallinn, Estonia, June 2007.
[
dVT01] R. G. de Vries and J. Tretmans. Towards formal test purposes.
In Proceedings of 1st International Workshop on Formal Approaches to Testing of Software 2001 (FATES'01) , volume NS-01-4 of BRICS Notes Series, pages 61-76, Aarhus, Denmark, August 2001.
[
EPG*07] M. D. Ernst, J. H. Perkins, P. J. Guo, S. McCamant, C. Pacheco, M. S. Tschantz, and C. Xiao. The Daikon system for dynamic detection of likely invariants.
Science of Computer Programming , 2007.
[
FMP03] J.-C. Fernandez, L. Mounier, and C. Pachon. Property oriented test case generation.
In Formal Approaches to Software Testing, Proceedings of FATES 2003, volume 2931 of Lecture Notes in Computer Science, pages 147-163, Montreal, Canada, 2004. Springer.
[
FB97] G. Fink and M. Bishop. Property-based testing: a new approach to testing for assurance.
SIGSOFT Softw. Eng. Notes, 22(4):74?80, 1997.
[
FTW04] L. Frantzen, J. Tretmans, and T. A. C. Willemse. Test generation based on symbolic specifications.
In Formal Approaches to Software Testing, Proceedings of FATES'04, volume 3395 of Lecture Notes in Computer Science, pages 1-15. Springer, 2005.
[
Gau95] M.-C. Gaudel. Testing can be formal, too. In Peter D. Mosses, Mogens Nielsen, and Michael I. Schwartzbach, editors,
Proceedings of Theory and Practice of Software Development -TAPSOFT95, volume 915 of Lecture Notes in Computer Science. Springer, 1995.
[
GLOA06] M. Grindal, B. Lindström, J. Offut, and S. F. Andler. An evaluation of combination strategies for test case selection.
Empirical Software Engineering, 11(4), 2006.
[
GPY02] A. Groce, D. Peled, and M. Yannakakis. Adaptive Model Checking.
In Tools and Algorithms for the Construction and Analysis of Systems : 8th International Conference, TACAS 2002, Held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2002, Grenoble, France, April 2002. LNCS.
[
GV03] A. Groce and W. Visser. What Went Wrong: Explaining Counterexamples.
In Proceedings of SPIN 2003, Portland, Oregon, 2003.
[
JJ04] C. Jard and T. Jéron. TGV: theory, principles and algorithms, a tool for the automatic synthesis of conformance test cases for non-deterministic reactive systems.
Software Tools for Technology Transfer (STTT), 6, October 2004.
[
LTX01] L. Lorentsen, A.-P. Tuovinen, and J. Xu. Modelling feature interactions in mobile phones.
In Feature Interaction in Composed Systems (ECOOP 2001), pages 7-13, Budapest, Hungary, 2001.
[
NE01] J. W. Nimmer and M. D. Ernst. Static verification of dynamically detected program invariants: Integrating Daikon and ESC/Java.
In Proceedings of RV'01, First Workshop on Runtime Verification, Paris, France, July 23, 2001.
[
PVY01] D. Peled, M. Y. Vardi, and M. Yannakakis. Black Box Checking.
J. Autom. Lang. Comb., 7(2):225-246, 2001.
[
PY07] M. Pezze and M. Young.
Software Testing and Analysis: Process, Principles and Techniques. Wiley, 2007.
[
SS06] A. Sinha and C. Smidts. Hottest: A model-based test design technique for enhanced testing of domain-specific applications.
ACM Trans. Softw. Eng. Methodol., 15(3):242-278, 2006.
[
Tre99] J. Tretmans. Testing concurrent systems: A formal approach.
In J.C.M Baeten and S. Mauw, editors, CONCUR'99 - 10th Int. Conference on Concurrency Theory, volume 1664 of Lecture Notes in Computer Science, pages 46-65. Springer-Verlag, 1999.
[
Tre96] Jan Tretmans. Test generation with inputs, outputs and repetitive quiescence.
Software - Concepts and Tools, 17(3):103-120, 1996.
[
UL06] M. Utting and B. Legeard.
Practical Model-Based Testing: A Tools Approach. Morgan Kaufmann, 2006.
[
VHB*03] W. Visser, K. Havelund, G. Brat, S. Park, and F. Lerda. Model checking programs.
Auto-mated Software Engineering Journal, 10(2), 2003.
[
Wil01] C. E. Williams. Towards a test-ready meta-model for use cases.
In Workshop of the pUML-Group held together with the UML 2001 on Practical UML-Based Rigorous Development Methods- Countering or Integrating the eXtremists, pages 270-287. GI, 2001.
2. Présentation
des partenaires
Brasilian Team
Participants:
- Patricia Machado,
Associate Professor at Departamento de Sistemas e Computação, Universidade Federal de Campina Grande (CV lattes)
- Augusto Sampaio,
Associate Professor at the Formal Methods Laboratory, Centro de Informática, Universidade Federal de Pernambuco (CV lattes)
- Paulo Borba,
Associate Professor, Centro de Informática, Universidade
Federal de Pernambuco (CV lattes)
- Alexandre Mota,
Associate Professor at Centro de Informática,
Universidade Federal de Pernambuco (CV lattes)
- Flavia Barros,
Associate Professor at Centro de Informática,
Universidade Federal de Pernambuco (CV lattes)
- Jorge Figueiredo,
Associate Professor at Departamento de Sistemas e Computação,
Universidade Federal de Campina Grande
(CV lattes)
- Sidney Nogueira, PhD Student at Centro de Informática, Universidade
Federal de Pernambuco
(CV lattes)
- Emanuela Cartaxo, Doctoral Student at Departamento de Sistemas e
Computação, Universidade Federal de Campina Grande
(CV lattes)
- Wilkerson Andrade, Doctoral Student at Departamento de Sistemas e
Computação, Universidade Federal de Campina Grande
(CV lattes)
- Cristiano Bertolini, Doctoral Student at Centro de Informática,
Universidade Federal de Pernambuco
(CV lattes)
- Rohit Gheyi, Post-doctoral research assistant at Departamento de
Sistemas e Computação, Universidade Federal de Campina Grande
(CV lattes)
The group is currently founded by CNPq/Brazil and Motorola Inc.
(as an industrial partner). Their main interests are devoted to the
practice and theory of testing and formal methods in the context
of embedded and concurrent/distributed applications, particularly
running on mobile phones. Mobile phone applications pose some
interesting challenges such as high-level interruptions in
multiprocessing architectures. The group is composed of 5
Professors, 2 Research Assistants, 6 PhD students, 8 Master
Students, 4 Undergraduate Students and one software developer.
Members are from UFPE and UFCG. Their research covers: (i)
Natural language processing tools for mapping natural language
sentences to formal specifications; (ii)
Test case
generation to generate the formal test cases, including
interruption test cases. (iii)
Test case selection
strategies that are needed due to the costs of test execution and
time-to-market. These strategies are applied to reduce the size of
generated test suites and redundancies, while keeping acceptable
coverage rates. (iv)
Reverse model engineering tools can
read a whole test suite written in Natural Language and obtain the
formal specification for each contained test case.
(v)
Model checking techniques are used to perform static
tests by comparing the model obtained from a reference
implementation against the model obtained from an implementation
under test, where both models are obtained through reverse
engineering. (vi)
Software product lines are identifying and
isolating the variability between software artifacts, such as the
use cases and the test specifications, improving the reuse and
modularity of these artifacts, avoiding duplication and other
common maintenance problems. (vii)
Test effort and capacity
estimation models to manage the test effort.
Several statistical techniques are used to create these models,
such as regression analysis, analysis of variance and simulation.
CV of Patrícia Machado
Patrícia Duarte de Lima Machado is a Professor in the Computing and Systems Department at Federal University of Campina Grande, Brazil, since 1995. She received her PhD Degree in Computer Science from the University of Edinburgh, UK, in 2001. The PhD was on formal aspects of software testing. She received her Master Degree in Computer Science from the Federal University of Pernambuco, Brazil, in 1994 and Bachelor Degree in Computer Science from the Federal University of Paraiba, Brazil, in 1992. She is currently the coordinator of the Brazilian Committee on Formal Methods and since 2004 she is one of the scientific leaders of the software engineering research group of her institution. Her research interests include software testing, formal methods, real-time systems and model-driven development.
Major publications of the brazilian team on the collaboration theme:
[
SM06] Daniel Aguiar da Silva and Patricia D. L. Machado. Towards test purpose generation from CTL properties for reactive systems.
Electr. Notes Theor. Comput. Sci. , 164(4):29-40, 2006.
[
MSM07] P. D. L. Machado, D. A. Silva, and A. C. Mota. Towards property oriented testing.
Electronic Notes in Theoretical Computer Science , 184C:3-19, 2007.
[
AB07] E. H. S. Aranha and P. Borba. An estimation model for test execution effort. In
1st International Symposium on Empirical Software Engineering and Measurement (ESEM 2007) , 2007.
[
BLM*07] D. L. Barbosa, H. S. Lima, P. D. L. Machado, J. C. A. Figueiredo, M. Juca, and W. L. Andrade. Automating functional testing of components from UML specifications.
International Journal of Software Engineering and Knowledge Engineering , 17:339-358, 2007.
[
CS06] G. Cabral and A. C. A. Sampaio. Formal specification generation from requirement documents. In
Brazilian Formal Methods Symposium - SBMF 2006 , pages 217-232, 2006.
[
FAM06] A. L. L. Figueiredo, W. L. Andrade, and P. D. L. Machado. Generating interaction test cases for mobile phone systems from use case specifications.
Software Engineering Notes , 31, 2006. Proceedings of A-MOST 2006.
[
MS02] P. D. L. Machado and D. T. Sannella. Unit testing for CASL architectural specifications. In
27th International Symposium on Mathematical Foundations of Compouter Science , volume 2420 of LNCS, pages 506-518. Springer, 2002.
French Team
Participants:
The Vertecs team of the Inria Research Center Rennes-Bretagne
Atlantique is focused on the use of formal methods to assess the
reliability, safety and security of reactive software systems. The
Vertecs team promotes the use of formal methods, i.e. formal
specifications of software artifacts and their required
properties, and mathematically founded validation methods. The
research of Vertecs covers several validation methods such as
verification (establish the correctness of
specifications with respect to requirements),
control synthesis ("forcing" specifications of
systems to stay within correct behaviours),
conformance testing (check the correctness of a real system
with respect to its specification),
and in particular automatic test generation of test cases
from specifications,
diagnosis and monitoring (detect erroneous
behaviours of a running system under partial observation).
Vertecs is also interested in combinations of these
techniques, both at the methodological level (combining several
techniques within formal validation methodologies) and at the
technical level (as the same set of formal verification techniques
- model checking, theorem proving and abstract interpretation -
are required for control synthesis, test generation and
diagnosis).
The research of the Vertecs team is concerned with the
development and study of the expressiveness of formal models, the
design of methods and tools, for verification, controller
synthesis, test generation and diagnosis that ensure desirable
properties (e.g. correctness, completeness, optimality, etc). It
is based on well-established theories: verification, model
checking, abstract interpretation, theorem proving, supervisory
control and conformance testing theories. The research carried out
by Vertecs tries to be as generic as possible in terms of models
and techniques in order to cope with a wide range of application
domains and specification languages.
The team has developed model-based testing tools: (i)
TGV
is a tool developed in collaboration with Verimag Grenoble for
test generation of conformance test suites from specifications of
reactive systems. It is based on the IOLTS model, the
ioco
testing theory, and on-the-fly test selection algorithms guided by
test purposes. An academic version is distributed in the CADP
toolbox (Inria Rhônes-Alpes). Another version had been
transferred in the SDL ObjectGéode toolset (Telelogic) but is no
longer maintained. A version extended with coverage based test
selection is distributed with the Agedis toolset for UML and the
IF language (Verimag). TGV is used in several places for research
(including in Brazil at UFCG) and teaching; and (ii)
STG
(Symbolic Test Generation) is a prototype tool for the generation
and execution of test case programs using symbolic techniques.
It uses the NBac tool for approximate analysis using
abstract interpretation. A new version is currently redesigned
in OCaml and is distributed from our Web page.
CV of Thierry Jéron
After a master in Mathematics obtained at the University of Rennes 1 in 1988,
Thierry Jéron did a master and a PhD in Computer Science in the IRISA laboratory.
The PhD was on theoretical and algorithmic aspects of verification, and it was defended in 1991.
He then spent one year as a research engineer in the Alcatel research lab near Paris,
working on verification and testing.
In 1993, he came back in IRISA as an INRIA research scientist
in the Pampa team where he worked for 8 years.
Since 2001, he is the scientific leader of the VerTeCS team.
He obtained his Habilitation in march 2004.
The current research interests of Thierry Jéron include verification,
model-based testing and diagnosis, security.
Major publications of the Inria team on the collaboration theme:
[
CJMR07] C. Constant, T. Jéron, H. Marchand, V. Rusu. Integrating formal verification and conformance testing for reactive systems. In
IEEE Transactions on Software Engineering , 33 (8): 559-574, 2007.
[
JJ05] C. Jard and T. Jéron. TGV: theory, principles and algorithms, a tool for the automatic synthesis of conformance test cases for non-deterministic reactive systems.
Software Tools for Technology Transfer (STTT) , 6, 2005.
[
PJJ*07] S. Pickin, C. Jard, T. Jéron, J.-M. Jézéquel, and Y. Le Traon. Test synthesis from UML models of distributed software.
IEEE Transactions on Software Engineering, 33(4), 252-269, 2007.
[
Rus03] V. Rusu. Combining formal verification and conformance testing for validating reactive sstems.
Journal of Software Testing, Verification, and Reliability, 13(3), September 2003.
[
CJJ07] C. Constant, B. Jeannet, T. Jéron. Automatic test generation from interprocedural specifications. In
TestCom/Fates07, Tallinn, Estonia, June 2007.
[
JJRZ05] B. Jeannet, T. Jéron, V. Rusu, and E. Zinovieva. Symbolic test selection based on approximate analysis. In
11th Int. Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'05), Edinburgh (Scottland), Volume 3440 of LNCS, April 2005.
[
JMR06] T. Jéron, H. Marchand, and V. Rusu. Symbolic determinisation of extended automata. In
4th IFIP International Conference on Theoretical Computer Science, IFIP book series, Stantiago, Chile, August 2006. Springer Science and Business Media.
[
Jer06] T. Jéron. Model-based test selection for infinite state reactive systems. In
5th IFIP Working Conference on Distributed and Parallel Embedded Systems, DIPES?06, Braga, Portugal. Springer SBM, October 2006.
[
ORT*07] M. Oostdijk, V. Rusu, J. Tretmans, R. de Vries, T. Willemse. Integrating verification, testing, and learning for cryptographic protocols. In
Integrated Formal Methods (IFM'07), 2007.
Collaboration history
Patricia Machado and Thierry Jéron met in 2003 during a french visit
organized by INRIA and COFECUB on the French side, and CAPES and CNPq on the Brasilian side. The meeting organized in Sao Carlos near Sao Paulo was focussed on testing activities.
In 2007 an Inria/CNPq collaboration proposal was proposed by our team,
and the teams of UFPE and UFCG.
The proposal is partly funded by Inria, but not by CNPq.
However, in the beginning of 2008, Sidney de Carvalho Nogueira and
Wilkerson de Lucena Andrade made a short visit (1 week) in Irisa.
Thierry Jéron was also invited in Brazil by Patricia Machado in August 2008 to give an invited talk at
SBMF in Sao Salvador.
3. Impact
The Brazilian and French teams are major actors of the research
community on model-based testing in their respective countries,
with a good international visibility. As can be seen from
descriptions of the team profiles,
the French and Brazilian teams share common interests. Both teams
are involved in research in formal methods, and in particular in
both model-based testing and formal verification. This is not so
common in the international context, even though more and more
verification teams get interested in testing. In fact, testing
(and even model-based testing) and verification are often seen as
separate problems. Our common point of view is that these problems
share a lot of features in terms of application domains, kind of
systems that are considered, models and underlying techniques that
can be used for crossfertilization. Moreover they can be combined
in several ways, some of which having already been explored by our
groups (e.g. verification techniques can be a tool for test
selection and testing can complete verification in undecidable
cases). These common views and orientations of our research should
thus be very profitable in the collaboration. Additionally, the
Brazilian and French teams are very close with respect to the
models and theories they consider, and they share common
knowledge on tools. They are both engaged in the four research
directions described in this proposal, with however different
points of view and focuses. Collaborating on these topics and
sharing their experience can thus be very fruitful for both teams.