Reactive Systems: Modelling, Specification and Verification
Reactive Systems: Modelling, Specification and Verification
复制标题
DOI：
--
复制
发表时间：
2007-08
期刊：
影响因子：
--
通讯作者：
L. Aceto;A. Ingólfsdóttir;K. Larsen;Jiri Srba
中科院分区：
文献类型：
--
作者：
L. Aceto;A. Ingólfsdóttir;K. Larsen;Jiri Srba
形式化方法是一个术语，用于描述使用数学逻辑的软件和软件系统的规范和验证。已经开发了各种方法并将其纳入软件工具中。一个重要的子类是分布式系统。有很多书研究了这种系统的特定方法，例如CSP，进程代数。这本书为研究生提供了一个更平衡的介绍，描述了各种方法，它们的优点和缺点，以及何时最好使用。介绍了米尔纳CCS及其操作语义，以及基于互模拟技术的行为等价概念和Hennessy-米尔纳模态逻辑的变体。在本书的后面部分，所提出的理论被扩展到考虑时间问题。这本书已经出现在冰岛和丹麦教授的各种课程，旨在给学生一个广泛的介绍该地区，与练习贯穿始终。
Formal methods is the term used to describe the specification and verification of software and software systems using mathematical logic. Various methodologies have been developed and incorporated into software tools. An important subclass is distributed systems. There are many books that look at particular methodologies for such systems, e.g. CSP, process algebra. This book offers a more balanced introduction for graduate students that describes the various approaches, their strengths and weaknesses, and when they are best used. Milner CCS and its operational semantics are introduced, together with notions of behavioural equivalence based on bisimulation techniques and with variants of Hennessy-Milner modal logics. Later in the book, the presented theories are extended to take timing issues into account. The book has arisen from various courses taught in Iceland and Denmark and is designed to give students a broad introduction to the area, with exercises throughout.