FORM-L: A MODELICA Extension for Properties Modelling Illustrated on a Practical Example

Abstract

As systems engineering methodologies for complex systems make increasing use of modelling and simulation techniques, it has become important to extend the MODELICA language to also cover requirements , and more generally, properties modelling. The ITEA2 MODRIO project is currently developing an extension for that very purpose: the FORM-L language (FOrmal Requirements Modelling Language). This paper presents an overview of the FORM-L concepts, and illustrates them with examples based on a practical case study, the Backup Power Supply (BPS) system. 1 Introduction Systems engineering methodologies for complex systems increasingly rely on, or could benefit from, modelling and simulation. For MODELICA to support activities such as functional validation of system requirements, design verification against requirements , testing, dysfunctional analyses and verification of operational procedures, the ITEA2 MODRIO project is developing extensions to the language. One of them concerns formal requirements and properties modelling, and is called FORM-L (FOrmal Requirements Modelling Language). This paper presents the main concepts underlying FORM-L, and illustrates them with examples taken from a MODRIO case study, the Backup Poser Supply (BPS) system. Section 2 presents the main objectives assigned to FORM-L. Section 3 introduces briefly the BPS case study in oder to provide a background context for the examples given in the floowing sections. Section 4 presents how FORM-L considers functions, constants and fixed variables. Section 5 introduces the notions of condition and event. Section 6 presents the notions of properties, requirements, assumptions and guards. Section 7 presents the notion of time locator, continuous or discrete. Section 8 presents how FORM-L views sets and arrays. Lastly, Section 9 presents how actions are modelled in FORM-L. 2 FORM-L Overview 2.1 Motivation Paper Innovative Modelling Architecture for the Verification of Design against System requirements presents how one of the methodologies developed by MODRIO (to verify the design of a system against its requirements) is supported by FORM-L. This includes in particular a clear separation of models serving different purposes in the systems engineering lifecycle or the support to systems operation. In particular, there should be a well-identified model that clearly and formally specifies: • The boundaries of the system under study. • The interactions of the system with its environment (including human operators), including any assumptions made regarding this environment. • The system requirements, including functional and timing requirements (concerning the interactions with the environment) and system operational requirements (including quality of service and fault-tolerance, and operational constraints aiming for example at reducing wear and tear of system components). 2.2 Main Notions This is supported by the FORM-L with the notions of property, requirement, assumption, and external information (to be supplied either by other MODE-LICA models or by engineering databases). The expression of a requirement or a desirable property needs to address four basic issues: WHAT, WHERE, WHEN (cf. EuroSysLib WP7.1 Property Modelling) and HOW WELL.