无线普适医疗应用程序的形式规范.pptVIP

无线普适医疗应用程序 的正式规范 1.内容介绍 1.引言与意义 2.正式方法 3.规范过程 4.案例研究 1.引言和意义 无线普适医疗应用程序是对功能正确性,可靠性,实用性和安全性提出严格要求的典型代表。与传统的安全关键应用程序相比之下，这种应用程序的无线和普适特性受用户和资源的运动及位置影响。 1.引言和意义 在本文中,主要完成以下几件事情： 介绍几种形式方法的基本框架； 对其中一些做了扩展； 介绍了一个无歧义规范的严格开发过程； 介绍一些规范的指引和规则。 本文的目的在于介绍一个包含规范过程和集成工具包的方法论，便于设计者设计无歧义及可证实的规范，以此来避免故障提高可靠性。 2．正式方法 1.正式实体。 2.环境微分 3.环境逻辑 4.实时瞬态逻辑 5.根据契约设计 2．正式方法 1.正式本体 一个本体包括： (1)定义本体中的类; (2)安排类的层次结构，(子类{超类); (3)定义关系; (4)找出类和实体之间的关系。 在我们的方法论中，本体被用来正式的明确的定义所有参与应用程序域设计的实体(如资源、服务、用户等) ，以及实体之间的关系。实体的关系通过指定它们的意思以及它们所满足数学属性(反身、传递、交换等等)来被正式定义为基元。 2．正式方法 2.环境微分 在环境微分中，所有的实体都被描述为进程。一类重要的进程是环境，这环境是一个用来计算的有边界的地方。一个环境界定出是和不是，包含和在内执行。 环境微分中n[P] 表示环境，n是环境名称，P是其内部运行的进程。进程“0”表示什么也不做。并行执行是用一个二元运算符“|”来表示，这是交换和关联的意思。“!P 代表P在其周围环境无限复制的过程。 2．正式方法 3.环境逻辑 环境逻辑中的逻辑规则有(1)那些定义命题的逻辑规则,如否定(?),析取(∧),和连接(∨);(2)一级逻辑规则：普遍量化(?)和存在量化(?);(3)除过普遍的时序逻辑规则：最终(◇)和总是(□)时序操作符;(4)空间操作符：如某处(?)和无处不在(△)。 在瞬时形态中关系P→P0，表明环境P可以通过使用一个简约原则变成P0。 同样,在空间形态的关系P↓P0，表明环境P一级嵌套包含P0。 2．正式方法 4.实时瞬态逻辑 不像它的名字，瞬时逻辑(例如环境逻辑)不提供有关时间定量的推理机制；你不能用它们来表达实时约束。 所以在本文中，我们将会提及实时瞬态逻辑(RTTL)，这是一个明确的时间形式主义，它通过使用一个特殊的变量T，来表示任何状态下的时间值以及使用一级量化变量来进行实时判断。 按照这种逻辑，公式： 意味着对于T0后的任何时间,α总是正确的。 2．正式方法 5.根据契约设计 契约式设计(DBC)[Meyer 1992]是一个依赖于正式契约规范的规范技术：契约条件必须贯穿于系统的生命中或在需要其服务之前，这样你可以使系统具有更高程度的可靠性。 从霍尔逻辑[霍尔1969]中得到的契约： 在DBC术语中，P是一个先决条件，Q是后置条件。契约指出，每当客户端验证调用服务时前提条件时，服务器将在执行结束后验证后置条件。如果客户端不调用前提条件，有关服务器执行后的状态是无法想象的。 3.规范过程 1.结构建模 2.行为建模 3.约束条件和特性建模 4.对于这个任务,我们推荐以下设计原则 3.规范过程 图1 建模过程 3.规范过程 1.结构建模 任务1.1定义了实体和关系.这个任务定义了一个本体来指代所有参与环境的实体(用户和资源)以及他们的关系. 任务1.2定义一个域。这个任务定义了一个环境的静态模型。这个模型是为了实现环境微分和描述实体之间的包含关系. 3.规范过程 2.行为建模 任务2.1定义运动。这个任务定义实体在环境中可表现的运动。这种运动被正式的规定为环境微积分中环境的功能。 任务2.2识别活动。这个任务指定在系统的支持下用户的所有活动的列表。 3.规范过程 2.行为建模 任务2.3定义操作。这个任务标识和正式定义了系统必须支持的基本操作。这样的操作代表了环境中执行活动的构建块并且可以用环境微分指定。 任务2.4指定活动。这个任务规定在任务2.2中定义了所有的活动。所有被环境支持的活动都被规定为基本操作的组成部分。这样，通过测