ABSTRACT

To take up those challenges, we propose to use a novel semi-formal approach based on transaction models. The merit of this approach is that it provides an easy and reliable abstraction to describe parallel components while being expressive enough to describe systems at different levels of abstraction. It possesses a rigorous formal semantics amenable to semi-formal verification and incremental refinement, and can thus be used to produce systems proven correct-by-construction.