This project aims at strengthening and consolidating an existing and fruitful collaboration in the area of software testing based on formal specifications. The considered specifications are in CIRCUS, a language developed in York, which integrates the notions of states and complex data types (in a Z-like style) and communicating parallel processes inspired from CSP.
Morover, the language comes with a formal notion of refinement and allows to take into account abstract specifications and their transitions to models of programs.
On the bases of the theory of formal software testing and the proof and test generation tools developed in LRI the project will address the following questions: What are the integrated testing strategies applicable to such languages, which combine aspects that have been studied separately, so far, with respect to testing?
How to justify these strategies and their coherence with the underlying test hypothesis? How to implement them in a well-founded way, starting from the existing proof and generation tools that exist in York and Orsay?