开发时间关键系统的经验——“生产单元”案例研究
软件工程
2014-04-07 v1 计算机科学中的逻辑
摘要
从 1994 年项目内部竞赛中使用的玩具生产单元的非正式需求描述出发，我们给出了一个尽可能贴近需求的规范说明。我们利用 Manna 和 Waldinger (1980) 的演绎程序综合方法，获得了一个经过验证的类 TTL 电路来控制该单元。该形式化规范也涵盖了机械方面，从而允许不仅对软件问题而且对机械工程问题进行推理。除了局限于带有显式连续时间的一阶谓词逻辑的方法外，本文还提出了一种尝试，即采用特定于应用的用户定义逻辑算子，以获得更简洁的规范和证明。
引用
@article{arxiv.1404.1198,
title = {Experiences in Developing Time-Critical Systems - The Case Study "Production Cell"},
author = {Jochen Burghardt},
journal= {arXiv preprint arXiv:1404.1198},
year = {2014}
}
备注
13 pages; 11 figures