控制器合成工具CTAV-TGA的功能扩展与优化
发布时间：2021-01-16 19:01
实时系统是指能够在指定或确定的时间内完成事件处理的计算机应用系统,其正确性不仅仅取决于其计算逻辑的正确性,并且与计算结果的产生时间有极大关系。在航空航天、生产控制、交通指挥、国防、核工业等安全攸关领域,实时系统发挥了至关重要的作用。因此保证实时系统的正确性和可靠性十分重要。模型检测是一种自动化地验证有限状态系统的技术。上世纪90年代,模型检测方法被应用到实时系统的可靠性和正确的检测上。模型检测针对的实时系统通常是封闭的,其运行结果只与系统自身的运行状态有关。然而在实际生活中,实时系统往往会间接或直接地受到外界因素的影响。因此我们需要合成一个控制器使得在外界因素影响下,系统仍然满足给定的性质,这就是控制器合成问题,它可以形式化的定义为:给定一个系统模型S和系统所需满足的性质Φ,是否存在一个控制器使得C（S）|=Φ。CTAV是一个基于时间自动机的实时系统模型检测工具。CTAV-TGA是在CTAV的基础上实现的以时间博弈自动机为模型的控制器合成工具。CTAV-TGA实现了以四种基本LTL性质<>p,[]p,[]<>p,<>[]p为获胜目标的控制器合成。但C...
【文章来源】：苏州大学江苏省
【文章页数】：67 页
【学位级别】：硕士
【部分图文】：
图１－１?一个简单的时间博弈自动机??
第二韋祛木概念?找制器合成工具ＣＴＡＶ－ＴＧＡ的功能扩展勹改进??第二章基本概念??开放实时系统的运行状态不仅取决于系统自身的行为，而且还受到外界环境因素??的影响。在模型检测方法中，通常使用时间自动机对实时系统进行建模，但时间自动??机中所有的动作都是可控的，无法模拟外界环境因素。因此我们采用时间博弈自动机??作为刻画开放实时系统的模型，利用时间博弈自动机中的不可控迁移模拟外界环境因??素。因此在本章中将介绍开放实时系统的概念，时间博弈自动机的相关理论，以及用??于描述性质的线性时序逻辑公式。??２．１开放的实时系统??实时系统指的是能够及时响应外部事件的发生，并且能在－定时限内快速完成对??事件的处理的计算机应用系统。实时系统的行为不仅依赖其计算逻辑的正确性，而且??事件的响应需要满足一定时间约束。模型检测所涉及的实时系统一般都是封闭的，在??进行模型检测时只需遍历状态空间，寻找不满足指定性质的路径或状态。而控制器合??成问题针对的是开放的实时系统，其运行结果不仅取决于自身的运行状态，还受到外??界因素的影响。图２－１中给出一个开放实时系统的例子。??贮藏室??ｎ??＿升降机??产出带??Ｉ?Ｉ??机械臂?２?—??１＝＾：．，．?］?生产器??供给带Ｕ?１??图２－１?—个简单的生产单元??以上图所示的一个用于生产盘子的生产单元［２１］为例，其生产原料通过供给带源源??８??
控制器合成工具ＣＴＡＶ－ＴＧＡ的功能扩展勹改进?第三章挖制器合成技术坫础??ｘ＝＝１０??ｘ＝０??ｙ＞＝２〇?一、??，＼?ｘ＝０，ｙ＝０?／?＼?ｘ＝０；ｙ＝０?ｆ’￣＾??Ｓｔａｒｔ?ｊ??＾?Ｌｏｏｐ?：?———Ｂａｄ??ｘ＜＝１０??图３－１时间自动机??３．２最大值抽象??在３．１节中定义过一个时间自动机ｄ的符号化语义模型为一个符号化迁移系统??八，Ｇ可能有无穷多个符号化状态。可以通过使用某种抽象［１３］方式，将迁移系统转??化为－？个冇穷状态迁移系统，从ｉｆｉ丨使得遍历状态空间称为可能，这是能够进行模型检??测以及控制器合成的基矗??如阁３－２中的时间自动机，它只有一个初始状态ａ，它的符号化辻移序列为：??Ａ－０?Ａ．ｖ＝０?Ａ．ｙ－ｖ＝〇＞?＾?＜ｃｉ，?１Ｓ６２八〇５．ｖ＾ｌ?八？ｖ－．ｖＭ〉＝＞?＜ａ，２：￡；ｃ５３?／＼０分５１?／＼ｘ－．ｖ＝２＞?＝＞?＜ａ，??３ＳｖＳ４八０￥＾?１八ｊｃ－ｊ＝３＞．．．。虽然榷十时钟带的符号化语义使得状态空Ｎ变为可数的，??但其状态空间依然是无穷的。每过去１个时间单元，循环就会发生－次，．Ｖ会被重置??为０，同时ｘ在不停的增长，从而导致了一个可数的，但是却无限的状态空间。??ｙ?■－?〇．?：：：：：??＼?ｒ?：＝?０?－?■＇?■１＇?＂?：?＾??…＜?ｄ＼／／／／／??Ｉ）?１?１?：ｉ?Ｉ?Ｘ??图３－２简单的时间自动机和它的状态空间??时间Ｇ动机的符号化语义可能引发一个无穷的迁移系统。设＃足时间自动机的－??个符号化状态（／，％中的时钟带。为了得到一个乜穷可达图，我们使用一Ａ抽象ａ：?Ｐ??１７??
【参考文献】：
期刊论文
[1]基于LTL语义的可达性控制器合成工具[J]. 景丽莎,项周坤. 计算机系统应用. 2016(11)
本文编号：2981363
【文章来源】：苏州大学江苏省
【文章页数】：67 页
【学位级别】：硕士
【部分图文】：
图１－１?一个简单的时间博弈自动机??
第二韋祛木概念?找制器合成工具ＣＴＡＶ－ＴＧＡ的功能扩展勹改进??第二章基本概念??开放实时系统的运行状态不仅取决于系统自身的行为，而且还受到外界环境因素??的影响。在模型检测方法中，通常使用时间自动机对实时系统进行建模，但时间自动??机中所有的动作都是可控的，无法模拟外界环境因素。因此我们采用时间博弈自动机??作为刻画开放实时系统的模型，利用时间博弈自动机中的不可控迁移模拟外界环境因??素。因此在本章中将介绍开放实时系统的概念，时间博弈自动机的相关理论，以及用??于描述性质的线性时序逻辑公式。??２．１开放的实时系统??实时系统指的是能够及时响应外部事件的发生，并且能在－定时限内快速完成对??事件的处理的计算机应用系统。实时系统的行为不仅依赖其计算逻辑的正确性，而且??事件的响应需要满足一定时间约束。模型检测所涉及的实时系统一般都是封闭的，在??进行模型检测时只需遍历状态空间，寻找不满足指定性质的路径或状态。而控制器合??成问题针对的是开放的实时系统，其运行结果不仅取决于自身的运行状态，还受到外??界因素的影响。图２－１中给出一个开放实时系统的例子。??贮藏室??ｎ??＿升降机??产出带??Ｉ?Ｉ??机械臂?２?—??１＝＾：．，．?］?生产器??供给带Ｕ?１??图２－１?—个简单的生产单元??以上图所示的一个用于生产盘子的生产单元［２１］为例，其生产原料通过供给带源源??８??
控制器合成工具ＣＴＡＶ－ＴＧＡ的功能扩展勹改进?第三章挖制器合成技术坫础??ｘ＝＝１０??ｘ＝０??ｙ＞＝２〇?一、??，＼?ｘ＝０，ｙ＝０?／?＼?ｘ＝０；ｙ＝０?ｆ’￣＾??Ｓｔａｒｔ?ｊ??＾?Ｌｏｏｐ?：?———Ｂａｄ??ｘ＜＝１０??图３－１时间自动机??３．２最大值抽象??在３．１节中定义过一个时间自动机ｄ的符号化语义模型为一个符号化迁移系统??八，Ｇ可能有无穷多个符号化状态。可以通过使用某种抽象［１３］方式，将迁移系统转??化为－？个冇穷状态迁移系统，从ｉｆｉ丨使得遍历状态空间称为可能，这是能够进行模型检??测以及控制器合成的基矗??如阁３－２中的时间自动机，它只有一个初始状态ａ，它的符号化辻移序列为：??Ａ－０?Ａ．ｖ＝０?Ａ．ｙ－ｖ＝〇＞?＾?＜ｃｉ，?１Ｓ６２八〇５．ｖ＾ｌ?八？ｖ－．ｖＭ〉＝＞?＜ａ，２：￡；ｃ５３?／＼０分５１?／＼ｘ－．ｖ＝２＞?＝＞?＜ａ，??３ＳｖＳ４八０￥＾?１八ｊｃ－ｊ＝３＞．．．。虽然榷十时钟带的符号化语义使得状态空Ｎ变为可数的，??但其状态空间依然是无穷的。每过去１个时间单元，循环就会发生－次，．Ｖ会被重置??为０，同时ｘ在不停的增长，从而导致了一个可数的，但是却无限的状态空间。??ｙ?■－?〇．?：：：：：??＼?ｒ?：＝?０?－?■＇?■１＇?＂?：?＾??…＜?ｄ＼／／／／／??Ｉ）?１?１?：ｉ?Ｉ?Ｘ??图３－２简单的时间自动机和它的状态空间??时间Ｇ动机的符号化语义可能引发一个无穷的迁移系统。设＃足时间自动机的－??个符号化状态（／，％中的时钟带。为了得到一个乜穷可达图，我们使用一Ａ抽象ａ：?Ｐ??１７??
【参考文献】：
期刊论文
[1]基于LTL语义的可达性控制器合成工具[J]. 景丽莎,项周坤. 计算机系统应用. 2016(11)
本文编号：2981363
本文链接：https://www.wllwen.com/kejilunwen/zidonghuakongzhilunwen/2981363.html
