Visual Component-Based Development of Formal Models

A4 Konferenspublikationer

Interna författare/redaktörer

Publikationens författare: S. Ostroumov, M. Waldén
Redaktörer: Mira Kajko-Mattsson, Pål Ellingsen, Paolo Maresca
Publiceringsår: 2017
Förläggare: Iaria xps press
Moderpublikationens namn: Third International Conference on Advances and Trends in Software Engineering (SOFTENG 2017)
Artikelns första sida, sidnummer: 43
Artikelns sista sida, sidnummer: 50
ISBN: 978-1-61208-553-1
ISSN: 2519-8394


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.

Senast uppdaterad 2020-04-08 vid 07:20