护理系论文提纲

论文题目：智能居家护理系统的形式化分析与验证

摘要：智能居家护理系统是生命攸关的系统,在部署前保证智能居家护理系统的正确性、安全性等至关重要。目前对系统进行验证主要采用传统检测方法和形式化方法。传统检测方法,如模拟和测试,人力和时间成本高,且不可能遍历所有状态,因此,无法保证系统的正确性、安全性等。形式化方法通过对系统建模,进行形式化描述,实现自动化验证,可以克服传统检测方法的不足。本文针对智能居家护理系统的功能和安全性验证提出了一种形式化分析、验证的方法,旨在发现智能居家护理系统设计缺陷,保证系统正确性、安全性及系统一致性,主要内容如下:首先,在现有研究的基础上提出智能居家护理系统的形式化建模框架,分别从系统环境和系统设计两方面对智能居家护理系统进行形式化建模。其次,提取出智能居家护理系统的关键属性和形式描述模型,根据属性需求对系统进行形式化描述,实现形式化验证,以发现系统设计缺陷,为改进系统设计提供依据。最后,为验证本文方法的可行性、有效性,以一个专为老年痴呆患者设计的智能居家护理系统SHCSFAP为实例,用PAT模型模拟检验工具对该系统进行了形式化建模及验证。实验结果表明本文方法在分析、检验智能居家护理系统方面是有效的。与现有研究相比,本文方法的特点如下:（1）使用STCSP（Stateful Timed CSP）、LTL（Linear Temporal Logic）、PAT工具,实现了智能居家护理系统的自动化验证。（2）由于STCSP语言支持对分层实时系统的建模,可以很好地描述和验证智能居家护理系统的分层、实时特性。（3）提取了智能居家护理系统的关键属性和形式描述模型。

关键词：形式化分析;建模;模型检验;智能居家护理系统;STCSP

学科专业：软件工程

摘要

ABSTRACT

第一章 绪论

1.1 研究背景及意义

1.2 国内外相关研究工作

1.3 论文的研究内容及主要工作

1.4 论文结构

第二章 智能居家护理系统

2.1 智能居家护理系统概述

2.2 SHCSFAP系统实例

2.2.1 SHCSFAP系统概述

2.2.2 感知层

2.2.3 中间层

2.2.4 应用层

2.3 本章小结

第三章 相关技术

3.1 形式化方法

3.1.1 形式化方法概述

3.1.2 形式化方法相关内容

3.1.2.1 形式化规约

3.1.2.2 形式化验证

3.2 STCSP语言

3.2.1 STCSP简介

3.2.2 STCSP基本语法及语义

3.3 线性时序逻辑语言（LTL）

3.3.1 LTL简介

3.3.2 LTL语法及语义

3.4 PAT工具

3.4.1 PAT简介

3.4.2 PAT中LTL的使用

3.5 本章小结

第四章 智能居家护理系统的形式化建模框架

4.1 系统环境模型

4.1.1 对用户行为建模

4.1.2 对环境实体建模

4.1.3 系统环境模型

4.2 系统设计模型

4.2.1 感知层的建模

4.2.1.1 通信模式的建模

4.2.1.2 感知模式的建模

4.2.1.3 感知层模型

4.2.2 中间层的建模

4.2.3 应用层的建模

4.2.4 系统设计模型

4.3 完整的系统模型

4.4 本章小结

第五章 智能居家护理系统的属性提取及建模

5.1 智能居家护理系统关键属性

5.2 正确性

5.2.1 规则的正确性

5.2.2 服务的正确性

5.3 安全性

5.3.1 无死锁性

5.3.2 守护服务

5.3.3 服务的有效性

5.4 系统一致性

5.5 本章小结

第六章 实验分析

6.1 系统模型

6.1.1 系统环境建模

6.1.2 系统设计建模

6.1.2.1 感知层建模

6.1.2.2 中间层建模

6.1.2.3 应用层建模

6.1.2.4 系统设计模型

6.1.3 完整的系统模型

6.2 系统验证

6.2.1 正确性

6.2.2 安全性

6.2.2.1 无死锁性

6.2.2.2 守护服务

6.2.3 系统一致性

6.3 实验结果及分析

6.4 本章小结

第七章 总结与展望

7.1 总结

7.2 展望

参考文献

致谢