NDLI: Automatic analysis of embedded systems specified in Astral

Content Provider	IEEE Xplore Digital Library
Author	Brink, K. Bun, L.J.G. van Katwijk, J. Lutje Spelberg, R.F. Toetenel, W.J.
Copyright Year	1998
Description	Author affiliation: Fac. of Tech. Math. & Inf., Delft Univ. of Technol., Netherlands (Brink, K.)
Abstract	A prerequisite for successful software development is the availability of a complete and consistent software requirements specification. One way to asses the correctness of requirements specifications is the application of formal verification. Recently, the verification tool Uppaal has become available. Uppaal performs automatic verification of properties of real-time systems through model-checking using timed automata. Timed automata have proved very useful in automatic analysis, but do not allow easy specification of requirements at a sufficiently high level. Astral is a formal specification language for (real-time) software requirements. Automatic analysis of specifications is very useful for generating feedback to the end-user pointing out errors in the specification or showing that it satisfies certain properties. The analysis improves the process of requirements elicitation and therefore increases Astral's usability. The paper reports on the authors' experiences using Uppaal for automatic analysis of Astral specifications. They discuss and evaluate a translation from Astral specifications into Uppaal's timed automata. Particular focus is on the transformation of Astral's maximal progress semantics into the semantic setting of the timed automata, which do not have a maximal progress semantics. They report on experience with automatic analysis of an Astral specification of the 'Generalised Railroad Crossing' example.
Starting Page	177
Ending Page	186
File Size	158816
Page Count	10
File Format	PDF
ISBN	0818682558
DOI	10.1109/HICSS.1998.656139
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	1998-01-09
Publisher Place	USA
Access Restriction	Subscribed
Rights Holder	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Subject Keyword	Embedded system Automata Programming Availability Application software Formal verification Real time systems Formal specifications Feedback Usability
Content Type	Text
Resource Type	Article

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

Automated Formal Verification and Testing of C Programs for Embedded Systems

Formal Specs Reuse with Embedded Systems Design Behavioral and Architectural Specifications in Real-Time Application Domains

Model-driven specification of component-based distributed real-time and embedded systems for verification of systemic QoS properties

Formal Semantics of the ProCom Real-Time Component Model

On Formal Modeling of TOPPERS Embedded Software

Formal verification of the PATHO real-time operating system

Formal analysis of attacks for e-voting system

Formal verification of the MetaH executive using linear hybrid automata

Model checking real-time component based systems with blackbox testing

Automatic analysis of embedded systems specified in Astral

Similar Documents

Automated Formal Verification and Testing of C Programs for Embedded Systems

Formal Specs Reuse with Embedded Systems Design Behavioral and Architectural Specifications in Real-Time Application Domains

Model-driven specification of component-based distributed real-time and embedded systems for verification of systemic QoS properties

Formal Semantics of the ProCom Real-Time Component Model

On Formal Modeling of TOPPERS Embedded Software

Formal verification of the PATHO real-time operating system

Formal analysis of attacks for e-voting system

Formal verification of the MetaH executive using linear hybrid automata

Model checking real-time component based systems with blackbox testing

Automatic analysis of embedded systems specified in Astral