NDLI: Executable formal models for validation and specless verification

Content Provider	IEEE Xplore Digital Library
Author	Greve, D. Wilding, M.
Copyright Year	2000
Description	Author affiliation: Rockwell Collins, Cedar Rapids, IA, USA (Greve, D.)
Abstract	Verification and certification of flight critical software and application-specific integrated circuits (ASICs) is currently a labor-intensive, manual process involving extensive testing, inspections, and process documentation. The complexity of these systems and devices will increase both because increases in cockpit automation and application integration offer important safety benefits and because astonishing improvements in digital computing technology can potentially improve performance and decrease cost. The current approach to verification and certification will be challenged by this increased complexity. In order to reap fully the benefits of these technological advances we must develop new methods for verification and certification of flight critical devices that provide higher degrees of assurance for increasingly complex systems while simultaneously streamlining the verification process. The development of executable formal models may offer higher degrees of assurance, address increased complexity, and streamline certain aspects of the verification process. Increased assurance can be obtained as a result of rigorous, mechanical, mathematically complete checks of consistency and completeness of system requirements as well as proofs of correctness of specific implementations. As vector-based testing becomes increasingly inadequate to assure correctness in the face of exponentially growing state space, formal proofs of correctness can encompass the entire design, demonstrating correctness once and for all.
File Size	766785
File Format	PDF
ISBN	0780363957
DOI	10.1109/DASC.2000.886875
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	2000-10-07
Publisher Place	USA
Access Restriction	Subscribed
Rights Holder	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Subject Keyword	Certification Circuit testing Application specific integrated circuits Integrated circuit testing Software testing Inspection Documentation Automation Application software Safety devices
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