NDLI: Use Case Maps as a property specification language

Content Provider	Springer Nature Link
Author	Hassine, Jameleddine Rilling, Juergen Dssouli, Rachida
Copyright Year	2007
Abstract	Although a significant body of research in the area of formal verification and model checking tools of software and hardware systems exists, the acceptance of these tools by industry and end-users is rather limited. Beside the technical problem of state space explosion, one of the main reasons for this limited acceptance is the unfamiliarity of users with the required specification notation. Requirements have to be typically expressed as temporal logic formalisms and notations. Property specification patterns were successfully introduced to bridge this gap between users and model checking tools. They also enable non-experts to write formal specifications that can be used for automatic model checking. In this paper, we propose an abstract high level pattern-based approach to the description of property specifications based on Use Case Maps (UCM). We present a set of commonly used properties with their specifications that are described in terms of occurrence, ordering and temporal scopes of actions. Furthermore, our approach also supports the description of properties with respect to their architectural scope. We provide a mapping of our UCM property specification patterns in terms of CTL, TCTL and Architectural TCTL (ArTCTL), an extension to TCTL, introduced in this research that provides temporal logics with architectural scopes. We illustrate the use of our pattern system for requirement specifications of an IP Header compression feature.
Starting Page	205
Ending Page	220
Page Count	16
File Format	PDF
ISSN	16191366
Journal	Software and Systems Modeling
Volume Number	8
Issue Number	2
e-ISSN	16191374
Language	English
Publisher	Springer-Verlag
Publisher Date	2007-12-07
Publisher Place	Berlin, Heidelberg
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Formal verification Temporal logic Property specification Use Case Maps Temporal and architectural scope Business Information Systems Information Systems Applications (incl.Internet) Programming Languages, Compilers, Interpreters Software Engineering Programming Techniques Software Engineering/Programming and Operating Systems
Content Type	Text
Resource Type	Article
Subject	Modeling and Simulation Software

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

UML specification of access control policies and their formal verification

Formalization of UML state machines using temporal logic

Procedure-modular specification and verification of temporal safety properties

Software engineering and formal methods

Formalizing requirements with object models and temporal constraints

Producing robust use case diagrams via reverse engineering of use case descriptions

Automated formal verification of visual modeling languages by model checking

Constraint-based test generation for automotive operating systems

Refactoring object constraint language specifications

Use Case Maps as a property specification language

Similar Documents

UML specification of access control policies and their formal verification

Formalization of UML state machines using temporal logic

Procedure-modular specification and verification of temporal safety properties

Software engineering and formal methods

Formalizing requirements with object models and temporal constraints

Producing robust use case diagrams via reverse engineering of use case descriptions

Automated formal verification of visual modeling languages by model checking

Constraint-based test generation for automotive operating systems

Refactoring object constraint language specifications

Use Case Maps as a property specification language