NotesFAQContact Us
Search Tips
Peer reviewed Peer reviewed
PDF on ERIC Download full text
ERIC Number: EJ1257499
Record Type: Journal
Publication Date: 2020
Pages: 16
Abstractor: As Provided
ISSN: ISSN-1648-5831
Scratch-Based User-Friendly Requirements Definition for Formal Verification of Control Systems
Grobelna, Iwona
Informatics in Education, v19 n2 p223-238 2020
Control systems are becoming ever more commonly used in everyday life. This is true both in industry and in the domestic domain, in the form of e.g., smart home systems. The quality of such systems can be increased by using formal verification methods, such as the model checking technique, to make sure that the designed system fulfills all user requirements. The requirements are usually written as temporal logic formulas. However, the technical skills of future users or the mathematical background knowledge of the developers are not always sufficient to support the essential stage of verification. In the paper we propose to use the Scratch-based user-friendly approach to define our own scenarios for a control system, in order to avoid focusing on the mathematical notation of temporal requirements. The specified properties can then be transformed into temporal logic formulas and used directly in the model checking process. Hence, the verification phase is simplified and more team members can participate in the engineering of requirements. An empirical study with students has shown that the proposed approach can be used in practice.
Vilnius University Institute of Mathematics and Informatics, Lithuanian Academy of Sciences. Akademjos str. 4, Vilnius LT 08663 Lithuania. Tel: +37-5-21-09300; Fax: +37-5-27-29209; e-mail:; Web site:
Publication Type: Journal Articles; Reports - Descriptive
Education Level: N/A
Audience: N/A
Language: English
Sponsor: N/A
Authoring Institution: N/A
Grant or Contract Numbers: N/A