Modeling and Testing Multi-Threaded Asynchronous Systems with Creol

Bosphorus bridge in Istanbul viewing from Asia to Europe.

After a long waiting period, yesterday our TTSS 2008 paper was published by Elsevier. The paper is a result of the CREDO project.

Bernhard Aichernig, Andreas Griesmayer, Rudolf Schlatte, and Andries Stam. Modeling and testing multi-threaded asynchronous systems with Creol. In Proceedings of the 2nd International Workshop on Harnessing Theories for Tool Support in Software (TTSS 2008), Istanbul, Turkey, 30 August 2008, volume 243 of Electronic Notes in Theoretical Computer Science, pages 3–14. Elsevier, July 2009. (PDF) (doi:10.1016/j.entcs.2009.07.002)

The paper describes a model-based testing technique for asynchronous, concurrent systems and shows how the modeling language Creol can serve as a test oracle. Creol is a nice object-oriented modeling language for distributed systems by University of Oslo. We applied the technique to a commercial agent-based information system.

The basic steps of our method are:

• Create an abstract model of the system under test (SUT) in Creol.
• Instrument the source code of the SUT by aspect-oriented programming techniques (here AspectC) for recording events.
• Execute tests on the SUT and record the events.
• Translate the event traces to Creol test cases.
• Replay the test case on the model.
• If successful: the test passed;
• If it fails: model check if there is a different non-deterministic path for this test case, if not the test failed.

Check out my other conference papers.

ICTAC 2010, Sept 1-3, Natal, Brazil

Photo courtesy of Dany Sakugawa

I have been invited to serve on the Program Committee of ICTAC 2010.

It will have a special track on Formal Testing Approaches headed by Marie-Claude Gaudel.

ICTAC 2010 is the 7th International Colloquium on Theoretical Aspects of Computing, the latest in a series founded by the International Institute for Software Technology of the United Nations University (UNU-IIST). ICTAC brings together practitioners and researchers to present their research and to exchange ideas and experience addressing challenges in both theoretical aspects of computing and in the exploitation of theory through methods and tools for system development.

The seventh edition of the event, ICTAC2010, will be held from the 1st to the 3rd of September, 2010, in Natal, Brazil.

ICTAC2010 will invite submissions of research papers of up to 15 pages and of tool papers of up to 6 pages. Research papers should contain original research, and sufficient detail to assess the merits and relevance of the contribution. Submissions reporting on industrial case studies are also welcome. Tool demonstration papers should stress the technical and practical side, illustrating how one can apply the theoretic contributions in practice. The schedule for submission and evaluation of papers is as follows.

Submission of abstracts: 08 March, 2010
Submission deadline: 15 March, 2010
Notification of acceptance: 30 April, 2010
Final version: 16 May, 2010

Semantics? Yes tester, you need it!

Once I had a testing project in industry in which we ran into the common situation that we did not know how to interpret a given requirement. Well, we asked the requirements manager for advice. Since it was a tricky question, he forwarded our request to the customer and to the developers. We were fortunate in getting quick responses. However, there was a problem: the answers were contradicting each other.

What had happened? Well, the customer and the developers had different interpretations of the requirements. There was a misunderstanding about this requirement. The consequence: the developers were implementing an incorrect system from the customers point of view.

So what about the tester? His understanding of the requirements is crucial. In the example above, the asking of us testers highlighted a serious problem. Without a clear understanding of the requirements, no reliable test verdict (pass or fail) can be given.

However, how do we know, if a tester understands the requirements? He could have made the same mistake as the developers. What if two testers (e.g. the customer's and the developer's) have different understandings of the requirements of a given SUT? Well, they would give different test verdicts: one might accept the SUT the other not. Is there a way to prevent such misunderstandings?

Not in general, because misunderstanding is a psychological process of wrong interpretation. However, we can limit the roots of such misinterpretations. We need to define the semantics, i.e. the meaning, of the requirements. And if nobody does it in a project, the tester should.

How do we define the semantics of requirements? Answer: by writing them in a formal notation with a precise semantics. There are modeling languages that come with a precise semantics, like VDM-SL, Z, B, Alloy, RAISE, CSP, LOTOS etc. These languages serve different purposes, but what they have in common is that their meaning is precisely defined, i.e. there is no ambiguity how to interpret what is written down.

Therefore, model-based testing should always apply models with a precise, formal semantics. Ok, most of the time a tester will not need it, because the meaning seems obvious, but as testers know, the rare cases matter. It even becomes more critical for model-based testing tools. If there is no precise standard semantics, different tools might behave differently for the same models. (A common problem of compilers for programming languages without precise semantics).

Here is my advice: if somebody tries to sells you a model-based testing technique, ask him if his notation has a formal semantics. If he answers positively, double-check and ask for formal proofs done in this notation. No proofs, no formal semantics. Don't accept notations with misunderstanding built in!

More on model-based testing with formal notations can be found in my publications.

Lecturing in China

From 2002 to 2006 I worked for the UN as a Research Fellow of UNU-IIST in Macao, a special administrative region of China. Part of the job was to hold advanced computer-science courses in developing countries. The participants were post-graduates, typically young assistant professors.

In 2003, at a course in Lanzhou I certainly got the most impressive welcome: my name on a banner at the entrance to the campus (see picture). In China protocol is important, but Lanzhou Jiatong University was special. As a UN representative I was also officially welcomed by the rector and interviewed by their campus TV. I must admit, I was slightly impressed. Even more so by the fact that they had their own hotel on campus in which I stayed.

The course title was Formal Methods in Software Development. Lanzhou Jiatong University, Lanzhou, China, December 15--19, 2003.

Teaching formal methods is fun!

The course participants.