## Time and Probability in Formal Design of Distributed SystemsDue to the current economic climate, many, if not all, industries depend upon computer systems for their product, design and manufacturing processes and for routine business functions. Although the use of such systems brings many advantages, the consequences of failure (including physical failure of computer systems, software design faults and human error) can involve both loss of life and environmental damage. safeguards and subsequent accountability. Research funds are accordingly being generated by governments and leading industries, affording the development of safety-critical systems by multi-disciplinary teams of mechanical, structural, electronic and software engineers and, where appropriate, psychologists, sociologists and economists. A new book series Real-Time Safety Critical Systems has been launched as a forum to enable all relevant researchers and developers (from industry and academia world-wide) to report their findings in the field. This publication is the first in the series and concentrates on presenting a framework for specification and analysis of real-time and reliability in distributed systems. The framework consists of a language for modelling the behaviour of distributed systems, a logic for formulating system properties, and an algorithm for verifying that descriptions in the language satisfy formulas expressed in the logic. is also accessible to readers with only a basic knowledge of formal modelling. Indeed, as Willem-Paul de Roever says in his introduction to the publication, it ... constitutes an indispensable link in the education of our next generation of researchers ... [and] ... gives a clear and scientifically responsible description how real-time and probability can be added to process algebra, how to extend Emerson and Clarke's branching time temporal logic to these new features, and how to verify the properties thus expressed by an appropriate tool |

### What people are saying - Write a review

We haven't found any reviews in the usual places.

### Common terms and phrases

action algorithm algorithms for labeling Alternating Bit Protocol Analogous axioms bisimilar bisimulation equivalent C(tr calculate command consider corresponding define Definition delay denotes DTMC environment equation exists finitely variable formula f fringe G{fix geometrically distributed Hence holds induction interrupt handler Intuitively label(tr labeled transition system labeled with f labeling transitions Lemma len(pc logic Markov Markov chain model checking operational semantics partial computation perform Ppar prefix probabilistic choice probabilistic transitions process G Proof properties Proposition protocol Pu tr reactive transitions Rºr satisfies Sched(R scheduler sched Scomp(sched Section semantics sender specify and verify t-parameter Table temporal logic Theorem throughput TPCCS expressions TPCCS process TPCTL formula TPWB transition diagram transition system transition trin transitions labeled trº Trr G units verification of average watchdog timer X-transition