We present a model based approach to the resolution of conflict between the many stakeholders involved in large scale information system deployment and use. The work is based on the authors experience of more than $20B of outsourcing contracts. The approach, rapid scenario planning (RaSP) yields concrete evidence of the underlying assumptions that drive design and deployment, as well as critical insights into systems and business dynamics. Social and long term management and governance benefits are also obvious. Our implementation of the methodology is supported by specific tools, however equivalent general purpose tools can be used to support this methodology.

We present a correction for an error that occurs in the following paper Formal Aspects of Computing (2006) 18:495-517.At first sight, the error appears to be simply a misplaced quantifier in the definition of bisimulation.We explain, however, that the error and its correction reveal a subtle interaction between the substructural connectives of MBI and the resource-process calculus SCRP.We begin with a specific example which illustrates the error.We include also the known typographical errors.We include also a statement of the consequences of these errata for the paper Electronic Notes in Theoretical Computer Science 172, 545-587, 2007, which builds directly upon Formal Aspects of Computing (2006) 18:495-517 and which illustrates the significance of these errata.

Abstract Recent advances in logics for reasoning about resources provide a new approach to compositional reasoning in interacting systems. We present a calculus of resources and processes, based on a development of Milner’s synchronous calculus of communication systems, SCCS, that uses an explicit model of resource. Our calculus models the co-evolution of resources and processes with synchronization constrained by the availability of resources. We provide a logical characterization, analogous to Hennessy–Milner logic’s characterization of bisimulation in CCS, of bisimulation between resource processes which is compositional in the concurrent and local structure of systems.

State-based models provide an attractive and simple approach to performance modelling. Unfortunately, this approach gives rise to two fundamental problems: (1) capturing the input loads to a system efficiently within such presentations; and (2) coping with the explosion in the number of states when the system is compositionally presented. Both problems can be regarded as searching for some optimal representative state model with a minimal cost. In this paper we present a probabilistic feedback search approach (popularly referred to as a genetic algorithm) for locating good models with low (state) cost.

Abstract. One of the major problems in modelling with process algebras is that of state explosion. With the addition of information describing duration, models become more exposed to growth in the size of the description of their behaviour. We describe a symbolic approach to the description of duration information within a probabilistic calculus that has two benefits: firstly we can describe behaviour without instantiating distributions; secondly we can control the growth in our system representation as a trade against model accuracy. We can compute upper bounds on performance without the inclusion of additional state information in our systems. A large example, from the discrete event simulation literature, is presented to demonstrate the effectiveness of the approach.

Abstract A probabilistic calculus, derived from Milner's SCCS, WSCCS is presented. We define a notion of bisimulation for probabilistic processes and show that it is a congruence. A simple equational characterisation is shown to be both sound and complete for finite processes. We present many examples including some extended ones. The larger examples show both the expressive power of WSCCS and the availability of simple proof methods for some complex systems.

Reactive, generative, and stratified models are considered within the framework of PCCS, a specification language for probabilistic processes. A structural operational semantics of PCCS, given as a set of inference rules for each of the models, a notion of bisimulation semantics, and some conference proofs are presented.>