“Keep it simple but not too simple” means that a complex solution is really a problem that's not very well understood. In formal methods, this is reflected not only in the size of the state space, but also in the dependencies between these states. This is the main reason why Formal Modelling is not delivering as expected: the state space explosion would require an infinite amount of resources. If an automated tool cannot handle the state space, how can we expect engineers to do so? This is where CSP comes in: it divides the state space in small manageable chunks, making it easier to reason about the behaviour. There are however a few pre-conditions for this to work: one must take a step back, dividing the complex state space before conquering it, hence thinking about functionalities and how they are related before thinking about the punctual states in space and time.

Extrapolating the CSP abstract process algebra leads to a generic concept of describing systems as a set of Interacting Entities, whereby the Interactions are seen as first class citizens, at the same level as the Entities, decoupling the Entities' states by explicit information exchanges. We enter hereby the domain of modelling. One major issue with modelling approaches is that, while we need different and complementary models to develop a real system, these often have different semantics (if the semantics are properly defined at all). By being able to hide the internal semantics, one can focus on the interactions and use these as standardised interfaces.

It is clear that for this to work in the software domain, the natural programming model should be concurrent and execute on hardware that is compatible with it – a design feature of the transputer that has not been matched since. This opens the door to multi-domain modelling where, for example, parts of the system are continuous and other parts are discrete (as in executing a clocked logic). This gives us an interesting new domain of hybrid logic, a topic we want to explore further in a workshop at the conference.

This lecture will be guided by my own personal journey, starting with a spreadsheet to program a parallel machine, covering Peter Welch's courses in occam [1] and the formal development of our distributed RTOS. Slides used in the presentation can be downloaded from [2].