Time and Probability in Formal Design of Distributed Systems

Due 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. Pressure is consequently being mounted to match technical progress with 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. Aimed at engineers and researchers involved across the discipline, the book 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 "
 
Due 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. Pressure is consequently being mounted to match technical progress with 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. Aimed at engineers and researchers involved across the discipline, the book 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 "