软件验证 – 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构成,可以用于:
  • 接收到广播信号时进行转移
  • 转移时产生广播信号

GUI Guide

大概左上角的位置有三个tabs:Editor, Simulator, Verifier

  • Editor
  • Declarations 用于声明和初始化全局变量
  • Templates 建立状态机的图形结构
  • System declarations 用于声明一个系统中包含的templates
  • Simulator
  • 红色的点是当前所在location
  • 转移所代表的连线被红色标识
  • Verifier
  • 在Query一栏中输入逻辑语句,点击Check可以验证是否满足某个性质

基本语法

赋值与条件

  • Transition 被激活时对变量的赋值:val := 0
  • 判断 transition 是否可以被激活的条件(用于 guard):val == 0
  • 一般Java里可以使用的 bool 语句,用,分隔

性质验证

  • E<> p 存在一条路径使得性质p最终可以满足。
  • A[] p 对于所有路径性质p总是可以满足。
  • E[] p 存在一条路径使得性质p总是可以满足。
  • A<> p 对于所有路径性质p最终可以满足。
  • p --> q p满足时,q最终可以满足

Pacemaker Algorithms

Timers

  • VRP Ventricular Refractory Period
  • Ignore voltage above threshold (no sensed events)
  • LRI = AEI + AVI
  • Lower Rate Interval: the minimum ventricular rate
  • Atrial Escape Interval: the minimum delay between a ventricular event and an atrial event
  • Atrial-Ventricular Interval: the minimum delay between an atrial event and a ventricular event
  • URI Upper Rate Interval
  • The maximum paced ventricular rate
  • PVARP Post-Ventricular Atrial Refractory Period
  • The PVARP is the period after a sensed or paced ventricular event during which the atrial sensing circuit is refractory

Algorithms

  • AEI内没有AS,就产生AP
  • AVI内没有VS,就产生VP
  • If URI 还没有结束,就产生一段时间的extension
  • VRP内,所有电流事件被忽略
  • PVARP内,所有心房事件被忽略

Pacemaker-mediated Tachycardia PMT

  • Atrial Tachycardia Response
  • 由于pacemaker对atrial过速回应导致的ventricle过速
  • Endless Loop Tachycardia
  • PVC, Premature ventricular contraction
  • VS AS VP AS VP AS… ( VP VS循环 )

 

Leave a Reply

Your email address will not be published.