We found a match
Your institution may have access to this item. Find your institution then sign in to continue.
- Title
Formal verification of a telerehabilitation system through an abstraction and refinement approach using Uppaal.
- Authors
Arfi, Farid; Courbis, Anne‐Lise; Lambolais, Thomas; Bughin, François; Hayot, Maurice
- Abstract
Formal methods are proven techniques that provide a rigorous mathematical basis to software development. In particular, they allow the quality of development to be effectively improved by making accurate and explicit modelling, so that anomalies like ambiguities and incompleteness are identified in the early phases of the software development process. Semi‐formal UML models and formal Timed Automata models are used to design a telerehabilitation system through a practical approach based on abstraction and refinement. The formal verification of expected properties of the system is performed by the Uppaal tool. The motivation of this work is threefold: (i) showing the usefulness of formal methods to satisfy the validation needs of a medical telerehabilitation system; (ii) demonstrating our approach of system analysis through refinements to guide the development of a complex system; and (iii) highlighting, from a real‐life experience, the usefulness of models to involve the stakeholders all along the design of a system, from requirements to detailed specifications.
- Subjects
UNIFIED modeling language; TELEREHABILITATION; SYSTEM analysis; COMPUTER software development; REQUIREMENTS engineering; EMPLOYEE motivation
- Publication
IET Software (Wiley-Blackwell), 2023, Vol 17, Issue 4, p582
- ISSN
1751-8806
- Publication type
Article
- DOI
10.1049/sfw2.12128