A case study in requirement analysis of control systems using UML and B

Colin Snook; Leonidas Tsiopoulos; Marina Walden

A case study in requirement analysis of control systems using UML and B

Colin Snook, Leonidas Tsiopoulos, Marina Walden

Information Technology

Research output: Book/Journal/Report › Commissioned report › Professional

30 Downloads (Pure)

Abstract

When developing critical systems that should be highly dependable we need to ensure that these systems satisfy functional as well as safety requirements. This can be achieved by developing the system with a formal method in a stepwise manner and proving the correctness of each step. For industrial strength systems, though, we need a graphical interface to the formal method. In this paper we develop part of a microplate liquid handling workstation, where we express the informal requirements and the refinements in UML. We translate the UML diagrams to B-action systems with the tool U2B. In the B-action system formalism we then prove the correctness of the development using the provers of the tool Atelier B.

Original language	English
Publisher	Turku Center for Computer Science (TUCS)
ISBN (Print)	952-12-1174-1
Publication status	Published - 2003
MoE publication type	D4 Published development or research report or study

Publication series

Name	TUCS Technical Reports
Volume	533

Keywords

Formal Methods
Industrial Case Study
The B Method
Action Systems
UML
Tool Support

Access to Document

TR533Final published version, 253 KB

MATISSE: Methodologies and Technologies for Industrial Strength Systems Engineering (IST-1999-11435) (EU-project)
Walden, M., Sere, K., Troubitsyna, E., Petre, L., Boström, P., Tsiopoulos, L., Jansson, M. & Engblom, N.
01/05/00 → 28/02/03
Project: EU

Cite this

@book{603565974b44443cb725a1e5f7ebf175,

title = "A case study in requirement analysis of control systems using UML and B",

abstract = "When developing critical systems that should be highly dependable we need to ensure that these systems satisfy functional as well as safety requirements. This can be achieved by developing the system with a formal method in a stepwise manner and proving the correctness of each step. For industrial strength systems, though, we need a graphical interface to the formal method. In this paper we develop part of a microplate liquid handling workstation, where we express the informal requirements and the refinements in UML. We translate the UML diagrams to B-action systems with the tool U2B. In the B-action system formalism we then prove the correctness of the development using the provers of the tool Atelier B.",

keywords = "Formal Methods, Industrial Case Study, The B Method, Action Systems, UML, Tool Support",

author = "Colin Snook and Leonidas Tsiopoulos and Marina Walden",

year = "2003",

language = "English",

isbn = "952-12-1174-1",

series = "TUCS Technical Reports",

publisher = "Turku Center for Computer Science (TUCS)",

}

TY - BOOK

T1 - A case study in requirement analysis of control systems using UML and B

AU - Snook, Colin

AU - Tsiopoulos, Leonidas

AU - Walden, Marina

PY - 2003

Y1 - 2003

N2 - When developing critical systems that should be highly dependable we need to ensure that these systems satisfy functional as well as safety requirements. This can be achieved by developing the system with a formal method in a stepwise manner and proving the correctness of each step. For industrial strength systems, though, we need a graphical interface to the formal method. In this paper we develop part of a microplate liquid handling workstation, where we express the informal requirements and the refinements in UML. We translate the UML diagrams to B-action systems with the tool U2B. In the B-action system formalism we then prove the correctness of the development using the provers of the tool Atelier B.

AB - When developing critical systems that should be highly dependable we need to ensure that these systems satisfy functional as well as safety requirements. This can be achieved by developing the system with a formal method in a stepwise manner and proving the correctness of each step. For industrial strength systems, though, we need a graphical interface to the formal method. In this paper we develop part of a microplate liquid handling workstation, where we express the informal requirements and the refinements in UML. We translate the UML diagrams to B-action systems with the tool U2B. In the B-action system formalism we then prove the correctness of the development using the provers of the tool Atelier B.

KW - Formal Methods

KW - Industrial Case Study

KW - The B Method

KW - Action Systems

KW - UML

KW - Tool Support

M3 - Commissioned report

SN - 952-12-1174-1

T3 - TUCS Technical Reports

BT - A case study in requirement analysis of control systems using UML and B

PB - Turku Center for Computer Science (TUCS)

ER -

A case study in requirement analysis of control systems using UML and B

Abstract

Publication series

Keywords

Access to Document

Fingerprint

Projects

MATISSE: Methodologies and Technologies for Industrial Strength Systems Engineering (IST-1999-11435) (EU-project)

Cite this