Abstract
While standalone tools for verification and modeling have proven useful, their chosen formalism and description-language can at times be restrictive. We demonstrate how to use U PPAAL SMC to analyze controller systems consisting of Function Mockup Units (FMU) modeled in other tools, such as Matlab and Modelica. Apart from supporting FMI-FMU modules the newly added C interface can call any external function. The only requirement for sound analysis is statelessness and determinism of the external function. We demonstrate the expressive power by implementing the FMI-FMU master algorithm as a timed automata, interfacing with external, non-native and non-trivial Function Mockup Units (FMU). We also model two components in U PPAAL SMC exporting one of them as an FMU while keeping the other as a native component. Furthermore we demonstrate the first simulation environment for the Function Mockup Units, capable of checking bounded MITL properties.
Original language | English |
---|---|
Title of host publication | Proceedings - 2017 22nd International Conference on Engineering of Complex Computer Systems, ICECCS 2017 |
Number of pages | 9 |
Publisher | IEEE |
Publication date | 15 Feb 2018 |
Pages | 11-19 |
ISBN (Electronic) | 978-1-5386-2431-9 |
DOIs | |
Publication status | Published - 15 Feb 2018 |
Event | 22nd International Conference on Engineering of Complex Computer Systems (ICECCS) - Fukuoka, Japan Duration: 5 Nov 2017 → 8 Nov 2017 |
Conference
Conference | 22nd International Conference on Engineering of Complex Computer Systems (ICECCS) |
---|---|
Country/Territory | Japan |
City | Fukuoka |
Period | 05/11/2017 → 08/11/2017 |