属性序列图:形式语法和语义

在基于场景的软件工程中,时态逻辑被广泛地用来推理并发系统的正确性.模型检验技术允许自动检验系统模型和给定的属性之间的一致性,这些属性常用线性时态逻辑公式来表示.不幸的是,由于这些公式具有复杂的结构使得模型检验技术很难应用在工业实践中.属性序列图可以用来解决这种问题,它是一种基于场景的可视化的语言,容易理解并且具有较强的表达能力,能够克服当前工业中常用的符号中存在的诸多表达缺陷.为了能够完全清晰地描述和理解属性序列图,使其能够广泛地应用,给出其形式语法和基于B(u)chi自动机的形式语义,并进行了实例研究,讨论了其应用前景.     

PSC2GS:一个基于属性序列图的监控器生成工具

在开放和动态环境下,系统或环境的不安全的运行时变化可能为整个系统的正确执行埋下隐患,可能最终导致软件失效。基于监控器的软件运行时验证技术已经成为开放环境下侦测软件失效行为的基本方法,该工具采用了一种基于博弈论的从Property Sequence Charts(属性序列图)中自动生成监控器的方法。监控器被赋予多值语义:满足、无限可控、系统有限可控、系统紧急可控、环境有限可控、环境紧急可控以及违例。监控器可以提供足够的信息用来预测系统失效。正文中将描述一个名为"PSC2GS"的工具,该工具具有设计属性序列图、基于属性序列图生成博弈结构、基于博弈结构生成Aspect Oriented Programming(面向方面编程)代码(监控器)等一系列功能。PSC2GS提供的完全图形化的前端接口使软件设计者可以不用处理任何特殊的文本或者逻辑公式。     

Büchi自动机确定化分析工具

无限字自动机的确定化是理论计算机研究重要的一部分,在形式化验证,时序逻辑,模型检测等方面有重要应用.自Büchi自动机提出半个世纪以来,其自动机的确定化算法始终是其中的基础.有别于当初只是在理论上对其大小上下界的探索,利用日新月异的高性能计算机技术不失为一种有效的辅助手段.为了深入研究非确定性Büchi自动机确定化算法的实现过程,我们希望重点研究确定化过程中的索引能否继续被优化的问题,实现了确定化研究工具NB2DR.可以对非确定性Büchi自动机进行高效的确定化,并通过工具提供的分析其确定化过程来达到对其确定化算法改进的目的.通过对生成的确定性无限字自动机的索引的深入分析来探索相关索引的理论.该工具还实现了可以根据需要的Büchi自动机的大小与字母表参数,生成确定化的Rabin自动机族,亦可以反向根据需要的指定索引的大小来生成全部Büchi自动机族,测试生成无限字自动机的等价性等功能.     

一种基于自动机理论的LTL检验符号优化方法

模型检验是一种重要的形式化自动验证技术。检验一个模型是否满足LTL公式,可以把LTL公式转换为一个表示相同无穷状态序列的ω自动机,通过转换后的ω自动机与系统自动机的乘积判空来进行模型检验。由于自动机的体积是模型检验的一个关键性问题,为了得到尽可能小的自动机,在LTL公式转换为ω自动机之前,对LTL公式进行预处理来减少冗余,然后基于ROBDD,通过布尔技术优化自动机。     

面向事件图和事件时态逻辑的模型检验方法

针对目前没有适合直接对事件图模型进行性质规约的时态逻辑语言,提出一种基于事件的时态逻辑(event temporal logic,简称ETL).ETL以事件作为原子命题,根据事件图的特点增加了对事件取消操作、模型实例化、时间约束和同时事件优先级的表达能力,便于仿真领域的用户在模型检验过程中简洁地对基于事件图的模型应满足的性质进行描述.然后,在ETL公式和自动机理论的基础上,给出了面向事件图和ETL的模型检验方法来判断事件图模型是否满足ETL描述的性质规约.实例验证了ETL对事件图模型具有足够的表达能力以及该方法的有效性.     

带时间约束的UML序列图的分析工具

统一建模语言(UML)是一种多用途的可视化建模语言,它可用于软件系统的规约、可视化的构造和建档.UML序列图描述了交互对象间的协作,如在实时和分布式系统中通讯实体间的信息交互.与其它的规约和设计过程类似,UML序列图的规约也易出错,所以对它进行分析是很有必要的.文章描述了一个对带时间约束的UML序列图进行分析的工具.     

基于进程代数的UML序列图的形式语义

UML序列图用于建模实例间动态交互过程．但UML规范并没有给出其形式化的动态语义,这不利于对模型进行形式化验证和证明。本文把序列图中的事件动作及其执行序列映射为进程代数中的进程表达式,利用进程代数语义框架来构建UML序列图的形式语义。首先,建立了序列图到进程代数的语义映射规则;然后用Plotkin风格的结构化操作语义给出并证明务件组合算子演绎规则;最后,归纳定义了算子次序约束条件并证明了其可终止性。     

面向参数化LTL的预测监控器构造技术

介绍了一种基于自动机理论的参数化LTL(parameterized LTL(linear temporal logic),简称P_ALTL)公式运行时预测监控器构造方法.一方面研究P_ALTL公式的语法、预测语义、赋值提取以及赋值绑定等重要概念,从语法层面保证公式中参数化变量的正确绑定(binding)和使用(using);另一方面给出参数化预测监控器的概念.它由静态和动态两部分组成,静态部分由参数化Büchi自动机表示,动态部分为当前状态处的变量赋值.在系统运行过程中,预测监控器基于静态部分的参数化Büchi自动机,以on-the-fly的方式在当前状态处动态地提取和绑定变量赋值,递进地验证当前程序运行是否满足指定的参数化性质规约.在该过程中,参数化监控器能够精确地识别被验证性质的最小好/坏前缀.     

基于事件确定有限自动机的UML2.0 序列图描述与验证

为了确保软件分析与设计阶段UML2.0序列图模型的可靠性,采用命题投影时序逻辑(propositional projection temporal logic,简称PPTL)模型检测方法对该模型进行分析和验证.提出了事件确定有限自动机(event deterministic finite automata,简称ETDFA),并使用该自动机为序列图建立形式化模型,通过给出的基于ETDFA的PPTL模型检测算法得到验证结果.该方法可以在基于Spin的PPTL模型检测器的支持下实现.实例结果表明,该方法可以验证序列图的性质并保证其可靠性.     

时间自动机与网络协议验证

随着网络协议复杂性的增大，其自身的潜在错误变得更加重要。使用形式化的方法来描述和验证网络协议可以发现其中的潜在错误。时间自动机是形式化方法的一种，可以很好地应用于网络协议验证中。目前基于时间自动机已经开发出了多种自动验证工具。文章介绍了网络协议验证的几种方法，并以KRONOS验证FDDI协议为例说明了用时间自动机验证协议的方法。     

Timed Property Sequence Chart

Property Sequence Chart (PSC) is a novel scenario-based notation, which has been recently proposed to represent temporal properties of concurrent systems. This language balances expressive power and simplicity of use. However, the current version of PSC just represents the order of events and lacks the ability to express timing properties. In real-time systems, it is well known that these timing requirements are very important and need to be specified clearly. Thus, in this paper, we define timed PSC (TPSC) and give the semantics of TPSC in terms of Timed Büchi Automaton (TBA). Then, we measure the expressive power of TPSC based on the recently proposed real-time specification patterns. Finally, we illustrate the use of TPSC in the context of a web service application which requires timing requirements.     

Semantics of Timed Message Sequence Charts

The paper describes an extended version of the well-known language of Message Sequence Charts (MSCs) with time specification of events. This extension is developed to verify requirements in interactive systems. To define the formal semantics of the language, a new approach based on the theory of interaction of agents and environments is used. Based on this semantics, an algorithm for checking the time consistency of MSCs is developed.     

Timed Semantics of Message Sequence Charts Based on Timed Automata

Message Sequence Charts (MSCs) provide a way for quick and easily understandable modelling of concurrent systems. Apart from their intuitive semantics easily deduced from their visual syntax, there is a formally defined semantics—Unfortunately, the semantics intuitively assigned to them is sometimes at odds with the formal semantics. In this paper, we will show an alternative approach to the semantics of MSCs, which will enable us to formally model their timed behaviour. Furthermore, we show how some generalizations of ordering events can lead to a language better suited to model real-world requirements. To ease the task of analyzing (High-Level) MSCs, we identify a subclass of those which can be translated into finite (timed of untimed) automata and specify the translation, thus laying the foundation for model checking.     

Monitoring of Probabilistic Timed Property Sequence Charts

Run‐time monitoring is an important technique to detect erroneous run‐time behaviors. Several techniques have been proposed to automatically generate monitors from specification languages to check temporal and real‐time properties. However, monitoring of probabilistic properties still requires manual generation. To overcome this problem, we define a formal property specification language called Probabilistic Timed Property Sequence Chart (PTPSC). PTPSC is a probabilistic and timed extension of the existing scenario‐based specification formalism Property Sequence Chart (PSC). We have defined a formal grammar‐based syntax and have implemented a syntax‐directed translator that can automatically generate a probabilistic monitor which combines timed B”uchi automata and a sequential statistical hypothesis test process. We validate the generated monitors with a set of experiments performed with our tool WS‐PSC Monitor. Copyright © 2011 John Wiley & Sons, Ltd.     

A Semantics for Timed MSC

Message Sequence Charts (MSC) is a graphical and textual specification language developed by ITU-T. It is widely used in telecommunication software engineering for specifying behavioral scenarios. Recently, the time concept has been introduced into MSC'2000. To support the specification and verification of real-time systems using timed MSC, we need to define its formal semantics. In this paper, we use timed lposet as a semantic model and give a formal semantics for timed MSC. We first define an event in a timed MSC as a timed lposet, then give a formal semantics for timed basic MSCs, timed MSCs with structures and high-level MSCs. In this paper, we also discuss some important issues related to timed MSC.     

An Operational Semantics for Timed CSP

An operational semantics is defined for the language of timed CSP, in terms of two relations: an evolution relation, which describes when a process becomes another simply by allowing time to pass; and a timed transition relation, which describes when a process may become another by performing an action at a particular time. It is shown how the timed behaviours used as the basis for the denotational models of the language may be extracted from the operational semantics. Finally, the failures model for timed CSP is shown to be equivalent to may-testing and, thus, to trace congruence.     

Intersection and Union Types: Syntax and Semantics

Type assignment systems with intersection and union types are introduced. Although the subject reduction property with respect to β-reduction does not hold for a natural deduction-like system, we manage to overcome this problem in two, different ways. The first is to adopt a notion of parallel reduction, which is a refinement of Gross-Knuth reduction. The second is to introduce type theories to refine the system, among which is the theory called Π that induces an assignment system preserving β-reduction. This type assignment system further clarifies the relation with the intersection discipline through the decomposition, first, of a disjunctive type into a set of conjunctive types and, second, of a derivation in the new type assignment system into a set of derivations in the intersection type assignment system. For this system we propose three semantics and prove soundness and completeness theorems.     

Combining Syntax and Semantics through Prime Form Representation

This article presents an algorithm that, besides calculatingthe number of models of a propositional logic theory, also determinesthe distribution of these models among the terms of a disjunctivenormal form representation of the theory. Using prime implicantsto represent the target theory, in a knowledge compilation context,we discuss how this distribution can be used to define beliefchange operators that respect the theory structure. Some experimentalresults are also presented.     

Syntax and Semantics for a Fuzzy Temporal Constraint Logic

In this paper we establish the relationship between the syntax and semantics of a fuzzy temporal constraint logic (FTCL) proposed by Cárdenas et al. FTCL enables us to express interrelated events by means of fuzzy temporal constraints. Moreover, it provides a resolution principle for performing inferences which take these constraints into account. FTCL is compatible with the theoretical temporal reasoning model proposed by Marín et al. – the Fuzzy Temporal Constraint Networks (FTCN). The main contributions of this paper are, on the one hand, the proofs of the FTCL-deduction and the FTCL-refutation theorems, and, on the other, the proof of the soundness of the refutation by resolution in this formal system, together with an exhaustive study of its completeness.