Designing, Modelling and Verifying a Container Terminal System Using UPPAAL

Author

Zu, Quan ; Zhang, Miaomiao ; Liu, Jing ; Du, Qingfeng

Author_Institution

Sch. of Software Eng., Tongji Univ.

fYear

2008

fDate

3-5 Dec. 2008

Firstpage

445

Lastpage

448

Abstract

This paper introduces an automated container terminal system which is used to transport containers from a ship to a yard. The system consists of a computation unit (CU) and several types of devices. The CU selects appropriate devices to transport the container. Due to the fact that the devices move concurrently and the intricate signals are exchanged between each device and the CU, it is very important to formally describe the system in a clear way. We thus present a method of modelling and analyzing the system in a model checker, UPPAAL. Through this work, the efficiency and correctness of the terminal system design is guaranteed.

Keywords

formal specification; formal verification; goods dispatch data processing; scheduling; systems analysis; UPPAAL integrated tool environment; automated container terminal system design; automated container terminal system modelling; automated container terminal system verification; computation unit; container transport; formal specification; model checker; real-time system; scheduling algorithm; timed automata; Algorithm design and analysis; Automata; Containers; Cranes; Design engineering; Machinery; Marine vehicles; Road transportation; Scheduling algorithm; Systems engineering and theory; Container terminal system; Model checking;

fLanguage

English

Publisher

ieee

Conference_Titel

High Assurance Systems Engineering Symposium, 2008. HASE 2008. 11th IEEE

Conference_Location

Nanjing

ISSN

1530-2059

Print_ISBN

978-0-7695-3482-4

Type

conf

DOI

10.1109/HASE.2008.35

Filename

4708903