SeminarPaperGearControllerCaseStudy.pdf资源-CSDN文库

需积分: 10 2 浏览量 2014-12-19 01:13:07 上传评论 1 收藏 290KB PDF 举报

### 关于实时系统工具UPPAAL的实例论文分析 #### 概述本文是一篇针对实时系统工具UPPAAL在工业应用中的实例研究。该研究主要聚焦在一个齿轮控制器（Gear Controller）的设计与分析上，该控制器是现代车辆控制系统的一个关键组成部分，负责执行换挡算法。研究者们来自瑞典的Mecel AB公司以及乌普萨拉大学计算机系统部门。通过合作项目的形式，他们共同探讨了如何利用UPPAAL这一验证和验证工具包来确保齿轮控制器设计的正确性。 #### UPPAAL工具介绍 UPPAAL是一款强大的模型检测工具，主要用于实时系统的建模、模拟及验证。它支持多种类型的模型，特别是时序自动机（Timed Automata）。时序自动机是一种广泛用于实时系统形式化方法的模型，能够描述系统的动态行为，并允许用户指定时间约束。UPPAAL不仅提供了一个图形界面方便用户构建模型，还提供了强大的模型检测引擎来验证系统的行为是否符合预期的安全性和活性属性。 #### 齿轮控制器案例研究在本案例中，研究人员为齿轮控制器建立了一个形式化的模型，并使用UPPAAL进行验证。具体来说： 1. **形式化模型**：根据工业合作伙伴提供的非正式需求，研究人员构建了一个详细的形式化模型，包括齿轮控制器本身及其运行环境。这个模型是用时序自动机表示的，并使用了线性时态逻辑（LTL）公式来正式化描述系统的正确性要求。 2. **响应时间属性验证**：研究中遇到了一个挑战，即如何利用仅提供可达性分析的UPPAAL工具来验证有界响应时间属性。例如，如果一个请求（事件）在某个时间点发生，则相应的响应必须在规定的时间范围内得到保证。为了解决这个问题，研究团队提出了一种逻辑和方法，通过语法转换和可达性分析来表征和验证这种属性。这种方法的优势在于不需要对现有的模型检测器进行额外的实现工作，而是通过对系统描述进行简单的手动语法操作来实现。 3. **验证过程**：使用安装在配备256MB主内存的Pentium 1GHz PC上的UPPAAL进行验证，整个过程只需要几秒钟就可以完成对LTL公式的检查。 #### 方法论为了实现上述目标，研究团队采用了以下步骤： 1. **需求分析**：从工业合作伙伴那里收集到非正式的需求规范。 2. **形式化模型构建**：基于这些需求构建时序自动机模型。 3. **LTL公式编写**：将需求规范转换为LTL公式，以便可以用UPPAAL进行验证。 4. **语法转换**：对模型进行适当的转换，以适应UPPAAL的可达性分析功能。 5. **模型验证**：使用UPPAAL对转换后的模型进行验证，确保满足所有的LTL公式。 #### 结论本研究展示了UPPAAL作为一种强大的验证工具在实际工业项目中的应用潜力。通过将非正式的需求规范形式化为时序自动机模型，并结合LTL公式，可以有效地验证齿轮控制器设计的正确性和响应时间属性。此外，研究提出的语法转换方法为解决特定类别的验证问题提供了一种有效途径，有助于减少模型检测器的开发工作量。这项研究不仅为齿轮控制器的设计提供了一种有效的验证方法，而且还为实时系统领域内的其他类似问题提供了一个有价值的参考案例。

资源推荐

资源详情

资源评论

Formal Design and Analysis of a Gear Controller:

an Industrial Case Study using U

PPAAL

Magnus Lindahl

Paul Pettersson

Wang Yi

Mecel AB, Goteborg, Sweden. E-mail:

magnus.lindahl@mecel.se

Department of Computer Systems, Uppsala University,Sweden.

E-mail:

paupet,yi

@docs.uu.se

Abstract.

In this pap er, we report on an application of the validation and verication tool

kit

Uppaal

in the design and analysis of a prototype gear controller, carried out in a joint

pro ject between industry and academia. The gear controller is a component in the control system

operating in a mo dern vehicle, implementing the gear change algorithm. We give a detailed

description of the formal mo del of the gear controller and its surrounding environment, and its

correctness formalized in 46 logical formulas according to the informal requirements delivered by

our industrial partner of the pro ject. The second contribution of this paper is a solution to the

problem we met in this case study, namely howtouseatoollike

Uppaal

, which only provides

reachability analysis to verify b ounded response time properties e.g.

(a request) becomes

true at a certain time point, then

(a response) must b e guaranteed to hold within a given

time b ound

.We present a logic and a metho d to characterize and model{check such properties

for networks of timed automata by syntactical transformation and reachability analysis. The

advantage of this approach is that we need no additional implementation work to extend the

existing mo del{checker, but simple manual syntactical manipulation on the system description.

The method has b een demonstrated in verifying the correctness of the gear controller design. It

takes 2.99 seconds to check the 46 logical formulas by

Uppaal

installed on a Pentium 75MHz

PC equipped with 24 MB of primary memory.

1 Intro duction

Over the past few years, a number of mo deling and verication tools for real-time systems [HHWT95,

DOTY95, BLL

96]have b een developed based on the theory of timed automata [AD94]. They have

been successfully applied in various case-studies [BGK

96, JLS96, SMF97]. However, the tools have

been mainly used in the academic community, namely by the to ol developers. It has b een a challenge

to apply these to ols to real-sized industrial case-studies. In this pap er we report on an application of

the verication to ol-kit

Uppaal

to a prototype gear controller developed in a joint pro ject between

industry and academia. The pro ject has b een carried out in collab oration between Mecel AB and

Uppsala University.

The gear controller is a component in the real-time embedded system that operates in a mo dern

vehicle. The gear-requests from the driver are delivered over a communication network to the gear

controller. The controller implements the actual gear change by actuating the lower level comp onents

of the system, such as the clutch, the engine and the gear-box. Obviously, the behavior of the gear

controller is critical to the safety of the vehicle. Simulation and testing have been the traditional ways to

ensure that the behavior of the controller satises certain safety requirements. However these metho ds

are by no means complete in nding errors though they are useful and practical. As a complement,

formal techniques have been a promising approach to ensuring the correctness of embedded systems.

The pro ject is to use formal mo deling techniques in the early design stages to describ e design sketches,

and to use symbolic simulators and mo del checkers as debugging and verication to ols to ensure that

the predicted behavior of the designed controller at each design phase, satises certain requirements

This work has been supp orted by ASTEC (Advanced Software TEChnology), NUTEK (Swedish Board for

Technical Development) and TFR (Swedish Technical Research Council).

under given assumptions on the environment where the gear controller is supp osed to operate. The

requirements on the controller and assumptions on the environmenthave b een describ ed by Mecel AB

in an informal do cument, and then formalized in the

Uppaal

model and a simple linear{time logic

based on the

Uppaal

logic to deduce the design of the gear controller.

We shall give a detailed description of the formal mo del of the gear controller and its surrounding

environment, and its correctness according to the informal requirements delivered by Mecel AB. An-

other contribution of this pap er is a lesson we learnt in this case study, namely howtouseatool like

Uppaal

, which only provides reachability analysis to verify b ounded resp onse time prop erties e.g.

(a request) b ecomes true at a certain time p oint,

(a resp onse) must b e guaranteed to b e true within

a time b ound

.We present a logic and a metho d to characterize and mo del{check resp onse time prop-

erties. The advantage of this approach is that we need no additional implementation work to extend

the existing mo del{checker, but simple manual syntactical manipulation on the system description.

Uppaal

is a tool suite for validation and symbolic mo del-checking of real-time systems. It consists

of a number of to ols including a graphical editor for system descriptions (based on Autograph), a

graphical simulator, and a symbolic mo del{checker. In the design phase the symbolic simulator of

Uppaal

is applied intensively to validate the dynamic behavior of each design sketch, in particular

for fault detection, derivation of time constraints (e.g. the time b ounds for which a gear change is

guaranteed) and later also for debugging using diagnostic traces (i.e. counter examples) generated by

the model{checker. The correctness of the gear controller design has b een established by automatic

proofs of 46 logical formulas derived from the informal requirements sp ecied by Mecel AB. The

verication was p erformed in a few seconds on a Pentium PC

running

Uppaal

version 2.12.2.

The pap er is organised as follows: Next section is a brief summary of various denitions for the

semantics and models of real{time systems. In section 3, we present a simple logic to characterize

safety and response time properties and a metho d to model{check such properties. In Section 4 and 5

the gear controller system and its requirements are informally and formally describ ed. In Section 6 the

formal description of the system and its requirements are transformed using the technique developed

in section 3 for verication by reachability analysis. Section 7 concludes the pap er. Finally,we enclose

the formal description of the surrounding environment of the gear controller in the app endix.

2 Preliminaries

In this section, we briey introduce all the necessary denitions for the basis of the

Uppaal

modelling

language. For details, we refer to [YPD94, LPY97].

2.1 Timed Transition Systems and Timed Traces

A timed transition system is a lab eled transition system with twotyp es of labels: atomic actions and

delay actions (i.e. p ositive reals), representing discrete and continuous changes of real-time systems.

Let

Act

be a nite set of actions and

be a set of atomic propositions. We use

to stand for the

set of non-negative real numbers,

for the set of delay actions



(

)

, and



for the union

Act

[

ranged over by

; 

;

etc.

Denition 1.

A timed transition system over

Act

and

is a tuple

S; s

;

, where

a set of states,

is the initial state,

,!







is a transition relation, and

is a

proposition assignment function.

A trace



of a timed transition system is an

innite

sequence of transitions in the form:





:::s



:::

Installation and do cumentation is available at the

Uppaal

home page

ttp://www.docs.uu.se/do cs/rtmv/uppaal/.

2.99 seconds on a Pentium 75MHz equipp ed with 24 MB of primary memory.

where





A p osition



is a natural number. We use



[

] to stand for the

th state of



, and



(

) for the

th transition of



, i.e.



[

and



(



We use



(



) to denote the duration of the transition, dened by



(



)=0if



Act





(

). Given positions

i; k

with



,we use



(

 ; i; k

) to stand for the accumulated delayof



between the positions

i; k

, dened by



(

 ; i; k



j<k



(



(

)). We shall only consider

non{zeno

traces.

Denition 2.

A trace



is non{zeno if for all natural number

there exists a position

such that

(

;

)

.For a timed transition system

,we denote by

(

)

all non{zeno traces of

starting

from the initial state

2.2 Timed Automata with Data Variables

We study the class of timed transition systems that can b e syntactically described by timed automata

extended with data variables ranging over nite data domains.

Assume a nite set of clo ckvariables

ranged over by

etc and a nite set of data variables

ranged over by

etc. We use

to denote the union of

and

, ranged over by

. We use

(

) to

stand for the set of formulas ranged over by

, generated by the following syntax:

::=

where

is a constraint of the form:



for

2 f

;



;

and

being a natural

number. We shall call elements of

(

)

guards

To manipulate clock and data variables, we use reset{operations of the form:

:= exp where

is a

clock or data variable and exp is an expression. A reset-op eration on a clo ckvariable should b e in the

form

:= 0; A reset-operation on an integer variable should be in the form:



where

k; k

are integer constants. We call a set of such reset{operations a

reset-set

.Areset{set is

proper

when

the variables are assinged a value at most once. We use

to denote the set of all proper reset-sets,

ranged over by

r;r

etc.

Denition 3.

A timed automaton

over actions

Act

, atomic propositions

, and

, is a tuple

L; l

;E;I;V

, where

is a nite set of no des (or lo cations),

is the initial no de, and



G

(

)



Act

R

corresponds to the set of edges. In the case,

l; g ; a; r;l

we shall write,

g;a;r

(

)

is a function which for each no de assigns an invariant condition, and

is a

proposition assignment function which for each no de gives a subset of atomic prop ositions true in the

node. We shall use

(

)

to stand for the union of the subsets of propositions true in all the nodes

, i.e.

(

)

Informally, a pro cess modelled by an automaton starts at its initial location

with all its variables

initialized to 0. The values of the clo cks increase synchronously with time at lo cation

.Atany time,

the pro cess can change lo cation by following an edge

g;a;r

provided the current values of the

variables satisfy the enabling condition

. With this transition, the variables are up dated by

variable assignment

is a mapping which maps clock variables

to the non-negative reals and

data variables

to integers. For a variable assignment

and a delay



denotes the variable

assignment such that (



)(

(

for any clockvariable

and (



)(

(

) for anyinteger

variable

. This denition of



reects that all clo cks op erate with the same sp eed and that data

variables are time-insensitive. For a reset-op eration

(a set of assignment-operations) we use

(

)to

denote the variable assignment

with

(

(exp

) whenever

:= exp

and

(

)

otherwise, where

(exp

) denotes the value of exp in

. Given a guard

2 G

(

) and a variable

assignment

(

) is a b oolean value describing whether

is satised by

or not.

2.3 Networks of Automata

To mo del concurrency and synchronization, weintro duce a CCS-like parallel composition operator for

automata. Assume automata

:::A

.We use

to denote their parallel comp osition

:::

. The

剩余17页未读，继续阅读

评论收藏

内容反馈

manu12

粉丝: 0
资源: 1

SeminarPaperGearControllerCaseStudy.pdf

HexView（Vector）V1.12.05

电池管理系统BMS原理图和源代码

MPU6050(OLED显示姿态角).rar

SecureCRT 9.0.0

Vivado2019.1安装包-百度网盘-22G.txt

CH340/CH341官方驱动最新版WIN11/10

MDK530.rar

cadence allegro 17.x 降版本到16.6的转换工具

PCIe规范各版本合集（1.0a、2.0、2.1、3.0、4.0、5.0）

softKeyBoard v1.0.0.rar

FPGA JFM7K325T官方中文技术手册.pdf

Keil.STM32F1xx_DFP.2.4.0.pack

TC397芯片参考手册和数据手册

JLink_Windows_V700.rar

CST仿真中文教程-图文并茂（适合小白入门）.pdf

几种USB type-c母座原理图符号及PCB封装（含3D模型，适用于AltiumDesigner）

GigaDevice_MCU_ISP_Programmer_V3.0.2.5782.zip

MIPI CSI-2 specification v3-0.pdf 2019最新版

OpenMV通信模块.rar

STM32F407 DAC + DMA + Timer 实现任意波形发生器

PCwin10蓝牙调试助手v1.00.rar

DDR5 JEDEC 官方标准 JESD79-5 DDR5 Spec _wrapper.pdf

IAR软件下载(附安装教程)

J1939协议(最全中文版).rar

IEC-61851-1-2017中文版

Keil.STM32F4xx_DFP.2.14.0.pack(官方STM32F4xx系列最新固件库for Keil MDK 5)

GD32+原理图与封装

Keil MDK STM32系列 PACK包

Keil.STM32F3xx_DFP.1.3.0.7z

最新资源