NDLI: Object Models with Temporal Constraints

Content Provider	IEEE Xplore Digital Library
Author	Cimatti, A. Roveri, M. Susi, A. Tonetta, S.
Copyright Year	2008
Description	Author affiliation: Fondazione Bruno Kessler, IRST, Povo (Cimatti, A.; Roveri, M.; Susi, A.; Tonetta, S.)
Abstract	Flaws in requirements often have a negative impact on the subsequent development phases. In this paper, we propose a novel formalism for the formal representation and validation of requirements. The formalism allows us to represent and reason about object models and their temporal evolution. The key ingredients are class diagrams to represent the objects in the scenarios, fragments of first order logic to deal with the relationships between their attributes and with rich data, and elements of temporal logic operators to deal with the dynamic evolution of the scenario.Formal validation is carried out by means of satisfiability checking, for which we propose a novel procedure based on the reduction to checking the language non-emptiness of a fair transition system.
Starting Page	249
Ending Page	258
File Size	394051
Page Count	10
File Format	PDF
ISBN	9780769534374
DOI	10.1109/SEFM.2008.23
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	2008-11-10
Publisher Place	South Africa
Access Restriction	Subscribed
Rights Holder	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Subject Keyword	Logic Application software Software engineering Constraint theory Decision feedback equalizers Surface-mount technology Software safety Software tools Formal languages Rail transportation
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

Scaling Up the Formal Verification of Lustre Programs with SMT-Based Techniques

Generalized, efficient array decision procedures

Using positive equality to prove liveness for pipelined microprocessors

Modeling wing level operations using formal object models

A scalable decision procedure for fixed-width bit-vectors

A formal approach to railway signalling

Propositional logic for validating software object interrelationships

Supporting Requirements Validation: The EuRailCheck Tool

Generation of object-oriented formal software specifications

Object Models with Temporal Constraints

Similar Documents

Scaling Up the Formal Verification of Lustre Programs with SMT-Based Techniques

Generalized, efficient array decision procedures

Using positive equality to prove liveness for pipelined microprocessors

Modeling wing level operations using formal object models

A scalable decision procedure for fixed-width bit-vectors

A formal approach to railway signalling

Propositional logic for validating software object interrelationships

Supporting Requirements Validation: The EuRailCheck Tool

Generation of object-oriented formal software specifications

Object Models with Temporal Constraints