首页 | 本学科首页   官方微博 | 高级检索  
     检索      


Asynchronous router specification
Authors:Moller  F
Institution:Dept. of Comput. Sci., Uppsala Univ.;
Abstract:We describe the application of three formal design tools to a case study in the design of a distributed system. The case study in question involves the specification of an asynchronous message router; the three design tools are process algebra (specifically Milner's Calculus of Communicating Systems CCS), the modal μ-calculus and the Edinburgh Concurrency Workbench (CWB). We demonstrate how an informally-presented specification can be formalised within the language of the modal μ-calculus, allowing for a rigorous mathematical analysis of the correctness of our proposed implementation. For modest-sized versions of the router, this correctness proof has been carried out using the CWB
Keywords:
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号