WCET Analysis of Superscalar Processors Using Simulation With Coloured Petri Nets

Determining a tight WCET of a block of code to be executed on a modern superscalar processor architecture is becoming ever more difficult due to the dynamic behaviour exhibited by current processors, which include dynamic scheduling features such as speculative and out-of-order execution in the context of multiple execution units with deep pipelines. We describe the use of Coloured Petri Nets (CP-nets) in a simulation based approach to this problem. A complex model of a generic processor architecture is described, with emphasis on the modelling strategy for obtaining the WCET and an analysis of the results.     

基于状态空间等价类的有色Petri网特性验证

在有色Petri网的状态空间中,有时一些状态具有相似的行为,这些状态可以用定义在状态空间上的一致的等价关系来表达,对每个等价状态类只研究它的一个代表状态的行为,这极大地减小了有色Petri网的状态空间。但是,通常对一个给定的等价关系是否为一致的验证都是通过用户的经验人工进行的,这不但容易产生错误,而且效率低下。该文依据普通状态图和等价类状态图的标记迁移系统关系,对状态空间一致性等价定义的计算机辅助验证做了深入的讨论,给出了相应的结果。     

时间Petri网分析工具的实现

时间Petri网是非常适合描述实时系统的模型工具,由于时间的复杂性因素使得它的可达性分析变得非常困难。该文在分析了基于全局时间变量的时间Petri网的可达性算法的基础上,采用OOP技术,实现了一个时间petri网的分析工具。     

Coloured Petri nets and graphical simulation for the validation of a robotic cell in aircraft industry

This paper proposes a mixed validation approach based on coloured Petri nets and 3D graphic simulation for the design of supervisory systems in manufacturing cells with multiple robots. The coloured Petri net is used to model the cell behaviour at a high level of abstraction. It models the activities of each cell component and its coordination by a supervisory system. The graphical simulation is used to analyse and validate the cell behaviour in a 3D environment, allowing the detection of collisions and the calculation of process times. The motivation for this work comes from the aeronautic industry. The automation of a fuselage assembly process requires the integration of robots with other cell components such as metrological or vision systems. In this cell, the robot trajectories are defined by the supervisory system and results from the coordination of the cell components. The paper presents the application of the approach for an aircraft assembly cell under integration in Brazil. This case study shows the feasibility of the approach and supports the discussion of its main advantages and limits.     

Modelling and analysing the functional behaviour of TCP’s connection management procedures

The transmission control protocol (TCP) is the most widely used transport protocol in the Internet. It provides a reliable data transfer service to many applications. In this paper, Coloured Petri Nets are used to model TCP’s connection management procedures. The model is created to verify TCP’s functional correctness (e.g. the absence of deadlocks and livelocks). We discuss different modelling approaches to motivate the approach taken. The paper defines the termination property of TCP’s connection management procedures, including the notions of desired and acceptable terminal states. Finally, we analyse TCP’s connection management procedures operating over re-ordering non-lossy and lossy channels. This is done incrementally and considers 11 different configurations. The analysis provides some insights into TCP’s behaviour where in certain circumstances the protocol fails to establish or terminate successfully. The majority of this article was written while Dr. Han was at the University of South Australia.     

自动组合装置赋时有色Petri网模型的建立分析

半导体制造中的自动组合装置是半导体制造的关键设备和瓶颈设备.对其性能进行量化的直观的分析对于半导体制造的效率和成本预测具有重要意义.文章阐述了如何利用Aarhus大学开发的CPN Tools对单臂双处理仓的自动组合装置建立赋时有色的佩特里网模型.文中按照不同建模思想建立起抽象型和具象型两个结构不同的模型,通过比对进行验证,最后利用CPN Tools自带的仿真功能进行仿真得出模拟运行的结果.文中的研究方法和结论对于复杂的自动组合装置的有色佩特里网的分析具有一定的参考价值.     

Modeling and formal verification of embedded systems based on a Petri net representation

In this paper we concentrate on aspects related to modeling and formal verification of embedded systems. First, we define a formal model of computation for embedded systems based on Petri nets that can capture important features of such systems and allows their representation at different levels of granularity. Our modeling formalism has a well-defined semantics so that it supports a precise representation of the system, the use of formal methods to verify its correctness, and the automation of different tasks along the design process. Second, we propose an approach to the problem of formal verification of embedded systems represented in our modeling formalism. We make use of model checking to prove whether certain properties, expressed as temporal logic formulas, hold with respect to the system model. We introduce a systematic procedure to translate our model into timed automata so that it is possible to use available model checking tools. We propose two strategies for improving the verification efficiency, the first by applying correctness-preserving transformations and the second by exploring the degree of parallelism characteristic to the system. Some examples, including a realistic industrial case, demonstrate the efficiency of our approach on practical applications.     

Improving state class constructions for CTL* model checking of time Petri nets

The state space explosion is still one of the most challenging problems in formal verification using enumerative techniques. The challenge is even greater for real time systems whose state spaces are generally infinite due to time density. To use enumerative techniques with these systems, their state spaces need to be contracted into finite structures that preserve properties of interest. We propose in this paper an efficient approach to construct a contraction of the time Petri net model state space, which preserves its CTL* properties.     

Tools and algorithms for the construction and analysis of systems

This special section contains the revised and expanded versions of eight of the papers from the 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) held in March/April 2004 in Barcelona, Spain. The conference proceedings appeared as volume 2988 in the Lecture Notes in Computer Science series published by Springer. TACAS is a forum for researchers, developers and users interested in rigorously based tools for the construction and analysis of systems. The conference serves to bridge the gaps between different communities – including but not limited to those devoted to formal methods, software and hardware verification, static analysis, programming languages, software engineering, real-time systems, and communications protocols – that share common interests in, and techniques for, tool development. Other more theoretical papers from the conference are collected in a special section of the Theoretical Computer Science journal.     

Model checking for process rewrite systems and a class of action-based regular properties

We consider the model checking problem for Process Rewrite Systems (PRS), an infinite-state formalism (non Turing-powerful) which subsumes many common models such as Pushdown Processes and Petri Nets. PRS can be adopted as a formal model for programs with dynamic creation and synchronization of concurrent processes, and with recursive procedures. The model-checking problem of PRS against action-based linear temporal logic (ALTL) is undecidable. However, decidability for some interesting fragment of ALTL remains an open question. In this paper, we state decidability results concerning generalized acceptance properties about infinite derivations (infinite term rewriting) in PRS. As a consequence, we obtain decidability of the model-checking problem (restricted to infinite runs) of PRS against a meaningful fragment of ALTL.