This book supports advanced level courses on concurrency covering timed and untimed CSP. The first half introduces the language of CSP the primary semantic models (traces, failures, divergences and infinite traces), and their use in the modelling, analysis and verification of concurrent systems. The second half of the book introduces time into the language, brings in the timed semantic model (timed failures) and finally presents the theory of timewise refinement which links the two halves together.
• Suitable for undergraduate and postgraduate courses on formal methods and software development.
• Written in a clear tutorial style of explanation.
• Contains numerous illustrative examples, exercises
and self-testing questions with solutions throughout.
• Relevant to users of any B-Method CASE tool.
[disclaimer: this is an inspection copy sent to me by the publisher]
This book provides a thorough and detailed understanding of one of the most effective approaches to the design and evaluation of security critical systems, describing the role of security protocols in distributed secure systems and the vulnerabilities to which they are prey.
The authors introduce security protocols, the role they play and the cryptographic mechanisms they employ, and progress to detail their role in security architectures, e-commerce, e-cash and so on. Precise characterizations of key concepts in information security, such as confidentiality, authentication and integrity are discussed and a range of tools and techniques are described which will ensure that a protocol guarantees certain security services under appropriate assumptions.