Author name cluster

W.P. de Roever

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

3 papers

1 author row

TCS Journal 1992 Journal Article

A compositional axiomatization of Statecharts

J.J.M. Hooman
S. Ramesh
W.P. de Roever

Statecharts is a behavioural specification language proposed for specifying large real-time, event-driven reactive systems. It is a graphical language based on state-transition diagrams for finite state machines extended with many features like hierarchy, concurrency, broadcast communication and time-out. We supply Statecharts with a compositional axiomatization for both safety and liveness properties. By generating external events symbolically, Statecharts can be executed, thereby turning it into a programming language for real-time concurrency (as well as enabling rapid prototyping). As such it is well suited for compositional program verification. In addition to our compositional axiomatic system, we give a denotational semantics and prove that the axiomatization is sound and relatively complete with respect to this semantics.

Details DOI

I&C Journal 1989 Journal Article

The μ-calculus as an assertion-language for fairness arguments

F.A. Stomp
W.P. de Roever
R.T. Gerth

Various principles of proof have been proposed to reason about fairness. This paper addresses—for the first time—the question in what formalism such fairness arguments can be couched. To wit: we prove that Park's monotone first-order μ-calculus, augmented with constants for all recursive ordinals can serve as an assertion-language for proving fair termination of do-loops. In particular, the weakest precondition for fair termination of a loop w. r. t. some postcondition is definable in it. The relevance of this result to proving eventualities in the temporal logic formalism of Manna and Pnuelis (in “Foundations of Computer Science IV, Part 2, ” Math. Centre Tracts, Vol. 159, Math. Centrum, Amsterdam, 1983) is discussed.

Details DOI

I&C Journal 1988 Journal Article

Compositional semantics for real-time distributed computing

R. Koymans
R.K. Shyamasundar
W.P. de Roever
R. Gerth
S. Arun-Kumar

We give a compositional denotational semantics for a real-time distributed language, based on the linear history semantics for CSP of Francez et al. Concurrent execution is not modelled by interleaving but by an extension of the maximal parallelism model of Salwicki and Müldner, that allows for the modelling of transmission time for communications. The importance of constructing a semantics (and, in general, a proof theory) for real-time is stressed by such different sources as the problem of formalizing the real-time aspects of Ada and the elimination of errors in the real-time flight control software of the NASA space shuttle (Comm. ACM 27 (1984)).

Details DOI