Specification, verification, and synthesis using extended state machines with callbacks
Specification, verification, and synthesis using extended state machines with callbacks
复制标题
使用带回调的扩展状态机进行规范、验证和综合
DOI：
--
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
Tuba Yavuz
中科院分区：
文献类型：
--
作者：
Farhaan Fowze;Tuba Yavuz
在本文中，我们使用在实际软件中高度使用的编程概念来扩展状态机图：回调机制。回调是与库交互的一种方式，可以以同步或异步模式的形式实例化。使用回调加快了软件开发速度，但代价是使程序理解复杂化。将回调概念引入建模形式化可以保持模型和实现之间的结构相似性。本文给出了这种扩展形式化的形式化语义，使其适用于形式验证和并发综合，并帮助开发人员避免实现错误，如竞争条件和死锁。我们报告了关于设备驱动程序的规范、验证和综合案例研究。
In this paper we extend state machine diagrams with a programming concept that is highly utilized in real software: the callback mechanism. A callback is a way to interact with a library and can be instantiated in the form of synchronous or asynchronous mode. Using callbacks speeds up software development at the expense of complicating program comprehension. Introducing the callback concept to a modeling formalism preserves structural similarity between the model and the implementation. This paper presents a formal semantics for this extended formalism to make it amenable to formal verification and concurrency synthesis and to help developers avoid implementation mistakes such as race conditions and deadlocks. We report specification, verification, and synthesis case studies on a device driver.