Stepwise development of Simulink models using the refinement calculus framework

Pontus Boström; Lionel Morel; Marina Walden

Stepwise development of Simulink models using the refinement calculus framework

Pontus Boström, Lionel Morel, Marina Walden

Information Technology

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

41 Downloads (Pure)

Abstract

Simulink is a popular tool for model-based development of control systems. However, due to the complexity caused by the increasing demand for sophisticated controllers, validation of Simulink models is becoming a more difficult task. To ensure correctness and reliability of large models, it is important to be able to reason about model parts and their interactions. This paper provides a definition of contracts and refinement using the action systems formalism. Contracts enable abstract specifications of model parts, while refinement offers a framework to reason about correctness of implementation of contracts, as well as composition of model parts. An example is provided to illustrate system development using contracts and refinement.

Original language	English
Publisher	Turku Centre for Computer Science (TUCS)
ISBN (Print)	978-952-12-1905-4
Publication status	Published - 2007
MoE publication type	D4 Published development or research report or study

Publication series

Name	TUCS Technical Report
Volume	821
ISSN (Print)	1239-1891

Keywords

Simulink
Design by Contract
Refinement
Action Systems

Access to Document

TR821Final published version, 299 KB

ITCEE: Improving Transient Control and Energy Efficiency by digital hydraulics (TEKES, KITARA-programme)
Walden, M. (Co-Principal Investigator), Sere, K. (Principal Investigator), Boström, P. (Co-Investigator), Morel, L. (Co-Investigator), Satpathy, M. (Co-Investigator), Olszewska, M. (Co-Investigator), Meincke, L. (Co-Investigator) & Malik, Q. (Co-Investigator)
01/08/05 → 31/07/08
Project: Industry/Business Finland

Cite this

@book{e0f2aed840ac48b393369fb3bebef80a,

title = "Stepwise development of Simulink models using the refinement calculus framework",

abstract = "Simulink is a popular tool for model-based development of control systems. However, due to the complexity caused by the increasing demand for sophisticated controllers, validation of Simulink models is becoming a more difficult task. To ensure correctness and reliability of large models, it is important to be able to reason about model parts and their interactions. This paper provides a definition of contracts and refinement using the action systems formalism. Contracts enable abstract specifications of model parts, while refinement offers a framework to reason about correctness of implementation of contracts, as well as composition of model parts. An example is provided to illustrate system development using contracts and refinement.",

keywords = "Simulink, Design by Contract, Refinement, Action Systems",

author = "Pontus Bostr{\"o}m and Lionel Morel and Marina Walden",

note = "Duplett till https://link.springer.com/chapter/10.1007/978-3-540-75292-9_6? EK 24/3/22",

year = "2007",

language = "English",

isbn = "978-952-12-1905-4",

series = "TUCS Technical Report",

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

}

TY - BOOK

T1 - Stepwise development of Simulink models using the refinement calculus framework

AU - Boström, Pontus

AU - Morel, Lionel

AU - Walden, Marina

N1 - Duplett till https://link.springer.com/chapter/10.1007/978-3-540-75292-9_6? EK 24/3/22

PY - 2007

Y1 - 2007

N2 - Simulink is a popular tool for model-based development of control systems. However, due to the complexity caused by the increasing demand for sophisticated controllers, validation of Simulink models is becoming a more difficult task. To ensure correctness and reliability of large models, it is important to be able to reason about model parts and their interactions. This paper provides a definition of contracts and refinement using the action systems formalism. Contracts enable abstract specifications of model parts, while refinement offers a framework to reason about correctness of implementation of contracts, as well as composition of model parts. An example is provided to illustrate system development using contracts and refinement.

AB - Simulink is a popular tool for model-based development of control systems. However, due to the complexity caused by the increasing demand for sophisticated controllers, validation of Simulink models is becoming a more difficult task. To ensure correctness and reliability of large models, it is important to be able to reason about model parts and their interactions. This paper provides a definition of contracts and refinement using the action systems formalism. Contracts enable abstract specifications of model parts, while refinement offers a framework to reason about correctness of implementation of contracts, as well as composition of model parts. An example is provided to illustrate system development using contracts and refinement.

KW - Simulink

KW - Design by Contract

KW - Refinement

KW - Action Systems

M3 - Commissioned report

SN - 978-952-12-1905-4

T3 - TUCS Technical Report

BT - Stepwise development of Simulink models using the refinement calculus framework

PB - Turku Centre for Computer Science (TUCS)

ER -

Stepwise development of Simulink models using the refinement calculus framework

Abstract

Publication series

Keywords

Access to Document

Fingerprint

Projects

ITCEE: Improving Transient Control and Energy Efficiency by digital hydraulics (TEKES, KITARA-programme)

Cite this