NDLI: Formal verification of requirements using SPIN: a case study on Web services

Content Provider	IEEE Xplore Digital Library
Author	Kazhamiakin, R. Pistore, M. Roveri, M.
Copyright Year	2004
Description	Author affiliation: DIT, Trento Univ., Italy (Kazhamiakin, R.; Pistore, M.)
Abstract	In this paper we describe a novel approach for the formal specification and verification of distributed processes in a Web service framework. The formal specification is provided at two different levels of abstraction. The strategic level describes the requirements of the Web service domain, in terms of the different actors participating to it, with their goals and needs and with their mutual dependencies and expectations. The process level shows how these requirements are operationalized into communicating processes running on the different Web servers. We model the strategic level exploiting Formal Tropos (FT), a language for the formal definition of the requirements of agent-oriented systems which is based on linear time logic. We model the process level using Promela, a language designed to describe communicating concurrent processes and amenable to formal verification. We exploit the SPIN model checker to perform V&V tasks. At the strategic level, requirements are validated against queries formulated by the designer while at the process level the Promela specifications are verified against the requirements. The implementation of these V&V tasks requires the definition of a novel procedure to encode the FT requirements in Promela. The experiments described in the paper show that the approach is effective in revealing possible flaws both in the strategic and in the process models.
Sponsorship	IEEE Comput. Soc. Tech. Comm. on Complexity in Comput
Starting Page	406
Ending Page	415
File Size	352719
Page Count	10
File Format	PDF
ISBN	076952222X
DOI	10.1109/SEFM.2004.1347546
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	2004-09-30
Publisher Place	China
Access Restriction	Subscribed
Rights Holder	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Subject Keyword	Formal verification Computer aided software engineering Web services Formal specifications Logic Software engineering Web server Programming Natural languages Performance analysis
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