软件验证 – UPPAAL&Pacemaker- 学习笔记

[ 官网 ] http://www.uppaal.org/

[ 参考文档 ] http://www.it.uu.se/research/group/darts/uppaal/small_tutorial.pdf

在智能医疗软件验证课上用Uppaal来搭建心脏和心脏起搏器模型,中文资料比较少,记录一下。

Basic Concepts

To begin with, 理解一个简单的概念:时间自动机(Timed Automate)一个基于时钟(clocks)的有限状态机(Finite State Machine)。每个状态叫做 location

  • 状态之间的转换叫做 transitions
  • 去激活(fire)一个转换,需要有一个转换条件(guard) 和状态间的同步( synchronization
  • Guard: 满足时一个转换(中文版翻译为“使能迁移”)才可以执行
  • Synchronization: 是由一些广播信道broadcast chan构成,可以用于:
  • 接收到广播信号时进行转移
  • 转移时产生广播信号

Continue reading “软件验证 – UPPAAL&Pacemaker- 学习笔记”