| 摘要: |
| LOTOS（languageoftemporalorderingspecification）是一种基于进程代数CCS的协议规范语言，面向协议验证，但它不能描述协议的某些性质．本文提出了一种LOTOS的扩充语言ELOTOS（extendedLOTOS），它在LOTOS的基础上引入了异步通讯机制、时间描述、事件发生的随机性描述． |
| 关键词: 协议规范语言 进程代数 LOTOS 实时系统 概率规范 |
| DOI： |
| 分类号: |
| 基金项目:本文研究得到国家自然科学基金和国家863高科技项目基金资助. |
|
| A SPECIFICATION LANGUAGE FOR FORMAL DEVELOPMENT ENVIRONMENT OF PRACTICAL PROTOCOLS |
|
LUO Tiegeng,CHEN Huowang,QI Zhichang,GONG Zhenghu
|
| Abstract: |
| LOTOS(language of temporal ordering specification) is a protocol specification language based on process algebra CCS. It is geared to protocol verification, but it is not powerful enough for describing some properties of practical protocols. This paper introduces a language ELOTOS(extended LOTOS), with the power of describing asynchronous communication, time, and stochastic event occurring. |
| Key words: Protocol specification language process algebra LOTOS real-time system probabilistic specification |
