A variety of research projects are in progress. These projects share the same philosophy of concurrency.

These projects are about:

  • Methodology
  • Programming
  • Designing (model-driven)
  • Verification (model-checking)
  • Concurrent thinking (cognition)

Our main project is the development of Waza. Other projects will be described here later.


If you are interested in a collaboration or a partnership, please contact us.

Formal foundation

Every formal aspect will be examined in detail using Communicating Sequential Processes (CSP). CSP is a theory of programming (process algebra) developed by Tony Hoare, Bill Roscoe and others. We also use other process algebras or process calculi, such as Algebra of Communicating Processes (ACP) by Jan Berstra and Jan Willem Klop, and Pi-calculus by Robin Milner. CSP is probably the simplest and most practical of all with a superior understanding of concurrency. In the near future, various types of model-checkers can be used to mathematically verify the program structures being developed with Waza.

Formal strategy

Safety critical software need to be trusted. Tests and model-checkers don’t cover all software. A practical strategy is required to cover most of the software and to provide (acceptable) guarantee of quality.

The Waza strategy uses a ‘program design synthesis by stepwise refinements’ and a ‘divide and connect, then conquer’ approach. Waza connects tests and model-checkers, at specific parts of the program design, in a concurrent way. For example, the nervous system of the program (the most sensitive part) can be verified using the CSP/ACP model-checker and the leaf components can be verified using unit tests or other tools. Every component must obey the simple semantics of processes and events. Waza incorporates a practical approach that is useful for software developers. This is our goal! The software developer can benefit from academic model-checkers without knowing about the process algebra. This is a powerful approach, which goes above and beyond objects and state-machines.