NDLI: Formal Verification of STATEMATE-Statecharts 1 Introduction

Please wait, while we are loading the content...

Formal Verification of STATEMATE-Statecharts 1 Introduction

Content Provider	Semantic Scholar
Author	Fuhrmann, Kay Hiemer, Jan
Abstract	During the software development process it is important to use powerful techniques for proving the expected behavior of the system and hence avoiding failures in real applications later on. Therefore, an effective means to increase confidence in the development process is to use analysis techniques based on the formal descriptions used in early phases (requirements specification). The'STATEMATE tool [HLN+90] is widely used for developing industrial software systems, e.g. avionic systems, automotive systems, computer operating systems etc. This paper concentrates on the STATEMATE-statecharts [Har87] as a description language for dynamic system behavior. Statecharts is a highly structured language extending conventional state transition diagrams by hierarchy, concurrency and communication. Within the STATEMATE tool users specify and validate these descriptions by a simulation tool which is driven interactively. Simulation is bounded in the way that it only shows some parts of a system and cannot provide evidence of requirements being satisfied over the whole life time of a system. The industrial practice of Statemate naturally leads to the point where developers require means for ensuring properties, e.g. the safety or security properties in avionic systems. Unfortunalety there are no practical tools implemented for such verification tasks. This paper introduces an approach which provides software engineers with fully automatic verification. Starting from a first system description of requirements the developer describes the dynamic behavior of the system in statecharts and formulates the requirements either as statecharts or as so-called temporal properties. Afterwards he can check automatically whether the system satisfies a requirement or not. Fig 1 shows our framework for translating statecharts and properties into a verification tool.
File Format	PDF HTM / HTML
Alternate Webpage(s)	https://page-one.springer.com/pdf/preview/10.1007/978-3-7091-6355-9_7
Language	English
Access Restriction	Open
Content Type	Text
Resource Type	Article

Central Library (ISO-9001:2015 Certified)
Indian Institute of Technology Kharagpur
Kharagpur, West Bengal, India | PIN - 721302

See location in the Map
03222 282435
Mail: support@ndl.gov.in

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in