具有动作细化的实时并发进程的基于事件的操作语义以及一致性结果

对于包含动作精化的实时进程代数，人们已经为它定义了指称真并发语义。在这种语义里，动作精化被看作是一个操作符。人们自然会有这样的疑问：既然已经定义了指称真并发语义，为什么还要定义操作语义?这个问题可以从以下两个方面回答：首先，对于不带时间变量和动作精化操作的进程，为它赋予一个“标准”语义的含义就是指为它定义一个操作语义。定义操作语义常用的方法是定义一个具有标记的传递系统，它是由一些推理规则组成的集合，这些推理规则刻画了实际程序或系统     

命令的指称语义在谓词域上的一种表示

文中讨论了谓词转换器和状态转换器之间的对应关系,将谓词转换器作为命令的指称,刻画了IMP语言命令的指称语义,并证明与状态转换器形式的指称语义是等价的.     

时间Petri网弱语义模型的形式化分析

时间Petri网存在强语义和弱语义两种模型,弱语义模型更适合建模和分析外部环境触发的冲突选择问题,但其形式语义和可达性分析方面的研究,却很少有人问津。利用带标号的变迁系统定义时间Petri网弱语义模型的形式语义,采用时间戳状态类方法分析它的可达性,并证明了可达性问题的可判性和状态类时间戳的全局时间性质。     

基于关键迹和ASP的CSP模型检测

模型检测是通信顺序进程(communicating sequential processes,简称CSP)形式化验证的重要手段.当前, CSP模型检测方法基于操作语义,需将进程转化为迁移系统,进而提取语义模型,但转化过程较为复杂;待验证性质采用CSP语言进行描述,虽然有利于精炼检测(refinement checking),但描述能力较弱,通用性不强.鉴于此,提出了一种新的CSP指称语义模型——关键迹模型(critical-trace model)及基于该指称语义模型的CSP模型检测方法,并证明了其验证的可靠性,避免了上述问题.关键迹模型采用递归策略计算,待验证性质采用线性时态逻辑(linear temporal logic,简称LTL)描述.基于回答集程序设计(answer set programming,简称ASP)实现了关键迹模型的自动生成及LTL的自动验证,并开发了一个CSP模型检测原型系统——T_ASP.实验结果表明:与类似系统相比,该系统的描述能力更强,验证结果的准确性更高,且可同时验证多条性质,在性质不满足时还可提供多条反例.     

基于标记变迁系统的可信计算平台信任链测试

可信计算是当今世界信息安全领域的重要潮流之一.根据国家有关规定,信息安全产品需要经过测评认证,但目前国内外对可信计算测试的理论与技术研究还非常不完善,也无相应测试工具或系统,这必然影响可信计算的发展.该文着眼于规范定义的信任链行为特征,以进程代数作为指称语义描述工具,以标记变迁系统作为操作语义,对规范定义的信任链行为特征进行了形式化描述,提出了一种基于标记变迁系统的信任链测试模型框架.针对信任链规范与实现之间的问题,从易测性出发对测试集进行了有效约简;并论证了信任链的规范实现与规范说明之间的关系,为测试用例构造方法提供了理论依据,从而解决了信任链测试这一难题.     

基于操作语义的磁臂隐通道分析*

深入分析磁臂隐通道的产生及产生的原因,发现目前基于系统顶级描述和基于系统源代码搜索方法难以找出这类隐通道,提出一种基于操作语义的方法来研究磁臂隐通道,将磁臂调度过程中的进程看做一个抽象机,以Plotkin的结构化操作语义给出电梯调度算法的推导规则;根据推导规则得到进程抽象机所有状态以及进程抽象机状态的动态变化历史,这样就构成完整的信息传导操作语义模型.研究与分析两个高低安全级进程抽象机状态变迁及状态变迁序列,从而找到其中存在的磁臂隐通道.     

一个面向对象的实时分布式语言的指称语义

本文给出了一个面向对象的实时分布式语言的指称语义，在不同层次Ｌ给出了语句、对象和程序的清晰描述．提出了实时状态的概念．借助于它，在指称语义的框架内，简洁地刻画了语言的实时特性．     

Tabular表达式的指称语义研究

Tabular 表达式是一种采用表格化结构组织函数或关系的形式化描述工具,在需求工程领域中具有广泛的应用,为Tabular 表达式建立形式的语义模型是非常必要的.针对Tabular 表达式通用模型,给出了Tabular 表达式的形式文法及指称语义.通过定义形式文法中各语法单元的语义指派方程,描述了Tabular 表达式的指称语义,分别对传统类型Tabular 表达式和新类型Tabular 表达式中一些典型表类型的指称语义进行了描述,并与其他几种Tabular 表达式的语义描述方法进行了比较.分析结果表明：该语义描述方法不仅准确描述了Tabular 表达式的语义,而且不再受Tabular 表达式模型和Tabular 表达式类型的限制,打破了现有方法的局限性,是一种非常有效的方法.     

基于扩展有限状态机模型的故障检测

提出了基于扩展有限状态机的故障检测模型和检测算法。该模型对软件中的故障进行了形式化定义和描述,检测算法对故障模型中的状态变迁进行缩减,检测故障模型的部分状态变迁,进而可以有效缓解状态空间过大而引起的时间和空间效率问题,从而最大限度地发现被测系统中的故障;最后给出了一个简单协议来加以分析和验证。实验表明,该算法可以快速准确地定位软件中故障发生的位置。     

Eiffel语言的语义

本文采用类ＶＤＭ的指称语义技术为Ｅｉｆｆｅｌ（１９８８）语言建立了形式语义模型．该模型首先为Ｅｉｆｆｅｌ语言定义了对象模型和两个语义环境（动态和静态环境）,然后讨论Ｅｉｆｆｅｌ例程的语义．为了描述Ｅｉｆｆｅｌ的意外处理,我们采用了ＶＤＭ的“出口”机制．     

UML活动图的操作语义

越来越多的系统采用UML（unified model language,统一建模语言）作为建模语言来进行系统分析和设计.UML活动图是UML语言中描述系统动态行为的一种方法,它广泛地运用于业务建模.由于UML活动图缺乏精确的动态语义,所以不利于对其所描述的系统进行形式化的分析、验证和确认.为解决这一问题,根据UML1.5语义文档,给出UML活动图的形式化操作语义.首先给出UML活动图的形式化的语法,然后详细地定义了活动图的格局和变迁,最后基于LTS给出了活动图的演绎规则.主要工作是：引入状态包的概念,使得描述更加清楚、完善;通过LTS定义活动图的操作语义,并详细阐述演绎规则,从而获得活动图的全局状态转移图,使定义的操作语义很容易地应用到形式化验证中.该语义覆盖了UML活动图的绝大部分特征,为对UML活动图进行模型检验奠定了基础.     

传值系统的互模拟与谓词等式系

本文引入描述传值并系统的新模型“带赋值符号迁移图（ＳＴＧＡ）”推广了Ｈｅｎｎｅｓｓｙ和Ｌｉｎ提出的“符号迁移图”的概念，允许迁移上带有赋值，从而能将更大的一类传值系统表示为有穷状态图，ＳＴＧＡ的中车优点是在并行运算不封闭，文中给给ＳＴＧＡ的操作语义，在此基础上定义了ＳＴＧＡ的互模拟等价关系，为了刻划ＳＴＧＡ的互模拟，以谓词等式系的形式在一阶逻辑的正子集中扩充了最大和最小不动点，并设计了一个算法将Ｓ     

A semantic framework for open processes

We propose a general methodology for analysing the behaviour of open systems modelled as coordinators, i.e., open terms of suitable process calculi. A coordinator is understood as a process with holes or placeholders where other coordinators and components (i.e., closed terms) can be plugged in, thus influencing its behaviour. The operational semantics of coordinators is given by means of a symbolic transition system, where states are coordinators and transitions are labeled by spatial/modal formulae expressing the potential interaction that plugged components may enable. Behavioural equivalences for coordinators, like strong and weak bisimilarities, can be straightforwardly defined over such a transition system. Different from other approaches based on universal closures, i.e., where two coordinators are considered equivalent when all their closed instances are equivalent, our semantics preserves the openness of the system during its evolution, thus allowing dynamic instantiation to be accounted for in the semantics. To further support the adequacy of the construction, we show that our symbolic equivalences provide correct approximations of their universally closed counterparts, coinciding with them over closed components. For process calculi in suitable formats, we show how tractable symbolic semantics can be defined constructively using unification.     

“Truly concurrent” and nondeterministic semantics of discrete-time Petri nets

In the paper, a “truly concurrent” and nondeterministic semantics is defined in terms of branching processes of discrete-time Petri nets (DTPNs). These nets may involve infinite numbers of transitions and places, infinite number of tokens in places, and (maximal) steps of concurrent transitions, which allows us to consider this class of DTPNs to be the most powerful class of Petri nets. It is proved that the unfolding (maximal branching process) of the DTPN is the greatest element of a complete lattice constructed on branching processes of DTPNs with step semantics. Moreover, it is shown that this result is true also in the case of maximal transition steps if additional restrictions are imposed on the structure and behavior of the DTPN.     

一种扩展了价格信息的时间Petri网

性能和成本分析是业务流程建模的主要目的,扩展了时间信息的Petri网能够有效地进行性能分析,但是对成本分析却无能为力.提出一种扩展了价格信息的时间Petri网--价格时间Petri网.首先为时间变迁扩展价格参数,并使用价格时间变迁系统给出价格时间Petri网的语义;然后提出计价状态类的概念,并证明为状态类扩展累积成本的合理性和完备性;进而给出一种算法来证明有界价格时间Petri网的最小成本可达问题是可判定的;最后给出一个应用例子并得出结论:为时间Petri网扩展价格信息并将其应用于业务流程管理领域是可行的.     

The effect of execution policies on the semantics and analysis ofstochastic Petri nets

Petri nets in which random delays are associated with atomic transitions are defined in a comprehensive framework that contains most of the models already proposed in the literature. To include generally distributed firing times into the model one must specify the way in which the next transition to fire is chosen, and how the model keeps track of its past history; this set of specifications is called an execution policy. A discussion is presented of the impact that different execution policies have on semantics of the mode, as well as the characteristics of the stochastic process associated with each of these policies. When the execution policy is completely specified by the transition with the minimum delay (race policy) and the firing distributions are of the phase type, an algorithm is provided that automatically converts the stochastic process into a continuous time homogeneous Markov chain. An execution policy based on the choice of the next transition to fire independently of the associated delay (preselection policy) is introduced, and its semantics is discussed together with possible implementation strategies     

Using Maude and Its Strategies for Defining a Framework for Analyzing Eden Semantics

Eden is a parallel extension of the functional language Haskell. On behalf of parallelism Eden overrides Haskell's pure lazy approach, combining a non-strict functional application with eager process creation and eager communication. We desire to investigate alternative semantics for Eden in order to analyze the consequences of some of the decisions adopted during the language design. In this paper we show how to implement in Maude the operational semantics of Eden in such a way that semantic rules can be modified easily. Moreover, other semantic features can be implemented by means of parameterized modules that allow to instantiate in different ways several parameters of the semantics but without modifying the semantic rules.     

Relational concurrent refinement part III: traces,partial relations and automata

Data refinement in a state-based language such as Z is defined using a relational model in terms of the behaviour of abstract programs. Downward and upward simulation conditions form a sound and jointly complete methodology to verify relational data refinements, which can be checked on an event-by-event basis rather than per trace. In models of concurrency, refinement is often defined in terms of sets of observations, which can include the events a system is prepared to accept or refuse, or depend on explicit properties of states and transitions. By embedding such concurrent semantics into a relational framework, eventwise verification methods for such refinement relations can be derived. In this paper, we continue our program of deriving simulation conditions for process algebraic refinement by defining further embeddings into our relational model: traces, completed traces, failure traces and extension. We then extend our framework to include various notions of automata based refinement.