● 摘要
在我们日常生活的各个方面,现代社会越来越依赖于专业的计算机和软件系统对于我们的协助。通常我们使用的手机,通信系统,医疗设备,音频和视频系统,以及家用电子产品一般都包含了大量的软件。一个常见的问题就是软硬件系统的复杂性不断增加,特别是有线和无线网络的使用更是加剧了这一趋势, 所以计算机科学领域遇到的一个主要的挑战就是提供方法,技术和工具以确保正确且功能良好系统的有效设计。在过去的大约二十年里,针对基于计算机控制系统正确性验证的一个非常好的方法那就是模型检测。究竟什么是模型检测?我们从两个不同的角度给出定义:1. 模型检测是一种主要的形式化验证技术用来评估信息和通信系统的功能性质;2. 模型检测是在合适的系统模型上对系统期望的性质进行验证,验证过程就是对模型中所有的状态进行系统化的检查。
随着科技的进步,模型检测技术也在持续发展,从开始的经典模型检测到概率模型检测,再到今天的多值模型检测,量子模型检测和可能性模型检测,许多专家学者对这种形式化验证技术从理论到实践都做了大量的研究。如何把模型检测理论应用到实践以解决实际问题对于我们来说是至关重要的,本文将应用自动机模型对多处理器任务调度算法进行建模与验证。
成本(或者是收益)是人们在决策系统中关注的焦点。对于非可加性的决策问题,本文建立了带有成本(收益)的可能性测度概念,并研究了其期望测度和多属性决策。
本文主要工作如下:
(1) 提出了一个基于扩展Büchi自动机的形式化模型,并用该模型来描述多处理器任务调度算法TDS(Task Duplication based Scheduling);用线性时序逻辑描述出算法TDS期望的一些性质;最后在该模型上验证了这些性质。
(2) 扩展了可能性Kripke结构——提出了带有成本的可能性Kripke结构,并且研究在此之上的期望测度和多属性决策问题。带有成本的可能性Kripke结构是在可能性Kripke结构的转移关系上(或者是状态上)给定了成本——这个自然数可以看成是成本,当然也可以看成是收益。本文中我们考虑转移关系上的成本。为了便于理解,我们会给出实例,将应用期望测度和最优化的理论来解决工程管理决策的相关问题。
相关内容
相关标签