Home // SOFTENG 2017, The Third International Conference on Advances and Trends in Software Engineering // View article

Visual Component-based Development of Formal Models

Authors:
Sergey Ostroumov
Marina Waldén

Keywords: Components Library; Visual Design; Event-B; Formal Components.

Abstract:
Formal methods, such as Event-B provide a means for system-level specification and verification supported by correctness proofs. However, the formal Event-B specification of a system requires background knowledge, which prevents a fruitful communication between the developer and the customer. In addition, scalability and reusability are limiting factors in using formal methods, such as Event-B in complex system development. This paper presents an approach to facilitate scalability of formal development in Event-B. Our aim is to build a formal library of parameterized visual components that can be reused whenever needed. Each component is formally developed and proved correct by utilizing the advantages of Event-B. Furthermore, each component has a unique graphical representation that eases the rigorous development by applying the “drag-and-drop” approach and enhances the communication between a developer and a customer. We present a subset of components from the digital hydraulics domain and outline the compositionality mechanism.

Pages: 43 to 50

Copyright: Copyright (c) IARIA, 2017

Publication date: April 23, 2017

Published in: conference

ISSN: 2519-8394

ISBN: 978-1-61208-553-1

Location: Venice, Italy

Dates: from April 23, 2017 to April 27, 2017