A framework for specifying and verifying the behaviour of open systems

We illustrate how the problem of modeling and verifying behavioural properties of open system is addressed by different research fields and how their results may contribute to a common solution. Building on this, we propose a methodology for modeling and verifying behavioural aspects of open systems. We introduce the IP-calculus, derived from the π-calculas process algebra so as to describe behavioural features of open systems. We define a notion of partial correctness, acceptability, in order to deal with the intrinsic indeterminacy of open systems, and we provide an algorithmic procedure for its effective verification.