嵌入式实时系统的软件需求检测

以需求描述模型HRFSM(hierarchical finite state machines based on rules)为基础,提出了一个嵌入式实时系统软件的动态执行模型(dynamic execution model,简称DEM)和基于该模型的检测方法.由于DEM能将控制流、数据流和时间有效地集成为一体,故提出的检测方法能检测嵌入式实时系统的软件需求的一致性和完全性.该检测方法由3种侧重点不同的检测形式组成,并能在检测过程中提供一些重要的检测信息.分析员可以利用基于该检测方法的工具灵活地对嵌入式实时系统的软件需求进行检测,以提高分析和检测软件需求的效率.     

改进的以SMT为基础的实时系统限界模型检测

基于SAT的限界模型检测在处理实时系统时具有很高的复杂度.SMT求解器在计算可满足性的同时,还能处理算术和其他可判定性理论.在对实时系统进行检测时,用SMT求解器代替SAT求解器,系统里的时钟就可以用整型或实型变量表示,时钟约束则可以直接表示成线性算术表达式,从而使整个检测过程更加高效.带时间参数的计算树逻辑(timed computation tree logic,简称TCTL)被用来描述实时系统里的性质.同时,还对检测方法作了相应的改进.     

改进的以SMT为基础的实时系统限界模型检测

基于SAT的限界模型检测在处理实时系统时具有很高的复杂度.SMT求解器在计算可满足性的同时,还能处理算术和其他可判定性理论.在对实时系统进行检测时,用SMT求解器代替SAT求解器,系统里的时钟就可以用整型或实型变量表示,时钟约束则可以直接表示成线性算术表达式,从而使整个检测过程更加高效.带时间参数的计算树逻辑(timed computation tree logic,简称TCTL)被用来描述实时系统里的性质.同时,还对检测方法作了相应的改进.     

基于Time Petri Net的实时系统冲撞检测与消解

time Petri net (TPN)在实时控制系统的建模中得到广泛应用,而冲撞是Petri网及其扩展模型的重要行为,解决冲撞是正确分析模型动态行为的关键.由于引入时间约束,使得TPN模型的使能和触发语义比Petri 网模型的语义复杂,冲撞的检测及消解变得更加困难.首先根据时间约束,给出了变迁持续使能时延迟区间的计算方法,并证明了该方法的正确性;然后在此基础上定义并证明了TPN模型中冲撞的检测方法;给出了冲撞时间区间及修改时间约束的冲撞消解方法;最后通过实例验证说明了该方法的有效性和正确性.     

基于线性时序逻辑的实时系统模型检查

模型检查是一种用于并发系统的性质验证的算法技术.LTLC(linear temporal logic with clocks)是一种连续时间时序逻辑,它是线性时序逻辑LTL的一种实时扩充.讨论实时系统关于LTLC公式的模型检查问题,将实时系统关于LTLC公式的模型检查化归为有穷状态转换系统关于LTL公式的模型检查,从而可以利用LTL的模型检查工具来对LTLC进行模型检查.由于LTLC既能表示实时系统的性质,又能表示实时系统的实现,这就使得时序逻辑LTLC的模型检查过程既能用于实时系统的性质验证,又能用于实时系统之间的一致性验证.     

网站实时监控和动态挖掘系统的研究与设计

本文提出并实现了一种对网上信息进行实时监控和对一些不良网站进行动态挖掘的系统,可以辅助相关部门对这些不良网站实行清理和打击,以净化因特网的信息空间.     

Exact Acceleration of Real-Time Model Checking

Different time scales do often occur in real-time systems, e.g., a polling real-time system samples the environment many times per second, whereas the environment may only change a few times per second. When these systems are modeled as (networks of) timed automata, the validation using symbolic model checking techniques can significantly be slowed down by unnecessary fragmentation of the symbolic state space. This paper introduces a syntactical adjustment to a subset of timed automata that addresses this fragmentation problem and that can speed-up forward symbolic reachability analysis in a significant way. We prove that this syntactical adjustment does not alter reachability properties and that it indeed is effective. We illustrate our exact acceleration technique with run-time data obtained with the model checkers Uppaal and Kronos. Moreover, we demonstrate that automated application of our exact acceleration technique can significantly speed-up the verification of the run-time behavior of LEGO Mindstorms programs.     

Event-Based Real-Time Monitoring

Real-time monitoring is required because of the uncertainty in the operating environment such as

(i) faulty hardware

(ii) the untrustworthiness of legacy and/or imported systems and

(iii) the violation of operational assumptions by the external environment, e.g., operator mistakes.

Different types of uncertainty may constrain the type of monitoring that can be performed. In this talk, we shall discuss the monitoring of non-functional properties such as timeliness and resource usage bounds, under the constraints imposed by the operating environment such as the uncertainty in the time of occurrence of events or the untrustworthiness of imported code.     

Real-Time Execution Monitoring

Today's programming methodology emphasizes the study of static aspects of programs. In practice, however, monitoring a program in execution, i.e., monitoring a process, is routinely done by any programmer whose task it is to produce a reliable piece of software. There are two reasons why one might want to examine the dynamic aspects of a program: first, to evaluate the performance of a program, and hence to assess its overall behavior; and second, to demonstrate the presence of programming errors, isolate erroneous program code, and correct it. This latter task is commonly called ``debugging a program' and requires a detailed insight into the innards of a program being executed. Today, many computer systems are being used to measure and control real-world processes. The pace of execution of these systems and their control programs is therefore bound to timing constraints imposed by the real-world process. As a step towards solving the problems associated with execution monitoring of real-time programs, we develop a set of appropriate concepts and define the basic requirements for a real-time monitoring facility. As a test case for the theoretical treatment of the topic, we design hardware and software for an experimental real-time monitoring system and describe its implementation.     

实时产生式系统

产生式系统是一种重要的人工智能程序设计语言,但却比较难于应用到实时领域之中.本文在分析其在实时应用方面两个主要不足的基础上,对实现实时产生式系统的几种可能途径与方法做了较为深入的探讨.     

并发反应式系统的组合模型检验与组合精化检验

模型检验和精化检验是两种重要的形式验证方法,其应用的主要困难在于如何缓解状态爆炸问题.基于分而治之的思想进行组合模型检验和组合精化检验是应对这个问题的重要方法,它们利用系统的组合结构对问题进行分解,通过对各子系统性质的检验和综合推理导出整个系统的性质.在一个统一的框架下对组合模型检验和组合精化检验作了系统的分析和归纳,从模块检验的角度阐述了上述两种组合验证方法的原理及其相应的组合验证策略.同时总结了各类问题的复杂性,并对上述两种方法作了比较分析,揭示了它们之间的内在联系.最后展望了组合模型检验与组合精化检验的发展方向.     

LDPChecker一个实时和混成系统模型检验工具

混成系统是一类复杂系统,线性混成系统作为其重要子类,在形式方法中,人们通常使用线性混成自动机来对它建模．虽然线性混成自动机的模型检验问题总的来说还是不可判定的,但对于其中的正环闭合自动机．其对于线性时段性质的满足性能够通过线性规划方法加以检验．为了实现自动检验正环闭合自动机对线性时段性质的满足性,设计并实现了工具LDPChecker．工具LDPChecker能够识别正环闭合自动机并对其进行相应的检验,其主要特色在于它能够对实时和混成系统检验包含可达性在内的许多实时性质,并且能够自动给出诊断信息．     

实时监控系统中H.264 模式选择算法的优化

由于实时监控系统对视频压缩的需要,本文针对H.264 标准的多模式运动估计算法编码模式复杂、计算量大的不足之处,在宏块编码模式选择统计规律的基础上,通过对纹理复杂度的分析,提出了一种利用预判法与部分模式排除法相结合的快速模式选择算法。该方法提前排除Skip 模式和inter16×16模式,再根据纹理复杂度将其余的模式分为两部分,对每部分包含的模式根据纹理方向再逐一排除,最后得到最优的模式。实验结果表明,本文提出的快速模式选择算法,在码率增加较小和视频质量损失不大的情况下,将编码时间平均缩短了76.95%。     

Scheduling of Time-Triggered Real-Time Systems

Thispaper introduces a new class of applications for constraint programming.This new type of application originates out of a special classof real-time systems, enjoying increasing popularity in areassuch as automotive electronics and aerospace industry. Real-timesystems of this kind are time triggered in the sense that theiroverall behavior is globally controlled by a recurring clocktick. Being able to compute an appropriate pre-runtime scheduleautomatically is the major challenge for such an architecture.What makes this specific off-line scheduling problem somewhatuntypical is that a potentially indefinite, periodic processinghas to be mapped onto a single time window. In this article wewill show how this problem can be solved by constraint programmingand we will describe which techniques from traditional schedulingand real-time computing led to success and which failed whenconfronted with a large-scale application of this type. The techniquesthat proved to be the most successful were special global constraintsand an elaborate search heuristics from Operations Research.Also for finding a valid schedule mere serialization is shownto be sufficient. The actual implementation was done in the concurrentconstraint programming language Oz.