16th BRAZILIAN SYMPOSIUM ON PROGRAMMING LANGUAGES (SBLP)
The Science of Killing Bugs in a Black Box
In this talk I will discuss the combination of model-based testing and mutation testing. Model-based testing is a black-box testing technique that avoids the labour of manually writing hundreds of test cases, but instead advocates the capturing of the expected behaviour in a model of the system under test. The test cases are automatically generated from this model. The technique is receiving growing interest in the embedded-systems domain, where models are the rule rather than the exception.
Mutation testing is a technique for assessing and improving a test suite. A number of faulty versions of a program under test are produced by injecting bugs into its source code. These faulty programs are called mutants. A tester analyses if his test suite can "kill" all mutants. We say that a test kills a mutant if it is able to distinguish it from the original. The tester improves his test suite until all faulty mutants get killed. In model-based mutation testing, we combine the central ideas of model-based testing and mutation testing: we inject bugs in a model and generate a test suite that will kill these bugs. In this talk, I will discuss its scientific foundations, tools, and results. The foundations include semantics and conformance relations; the supporting tools involve model checkers, constraint solvers and SMT solvers; our experimental results are taken from two European projects on embedded-systems. I will conclude with a proposal how model-based mutation testing can be integrated into an agile, iterative development process.
Software components as invariant-typed arrows
Invariants are constraints on software components which restrict their behavior in some desirable way, but whose maintenance entails some kind of proof obligation discharge. Such constraints may act not only over the input and output domains, as in a purely functional setting, but also over the underlying state space, as in the case of reactive com- ponents. This talk introduces an approach for reasoning about invariants which is both compositional and calculational: compositional because it is based on rules which break the complexity of such proof obligations across the structures involved; calculational because such rules are de- rived thanks to an algebra of invariants encoded in the language of binary relations. A main tool of this approach is the pointfree transform of the predicate calculus, which opens the possibility of changing the underlying mathematical space so as to enable agile algebraic calculation. The development of a theory of invariant preservation requires a broad, but uniform view of computational processes embodied in software compo- nents able to take into account data persistence and continued interaction. Such is the plan for this talk: we first introduce such processes as arrows, and then invariants as their types.