Article

Model Checking Early Requirements Specifications in Tropos

Authors:

Ariel Fuxman,

John Mylopoulos,

Marco Pistore,

Paolo TraversoAuthors Info & Claims

RE '01: Proceedings of the Fifth IEEE International Symposium on Requirements Engineering

Page 174

Published: 27 August 2001 Publication History

Publisher Site

Abstract

Abstract: This paper describes an attempt to bridge the gap between early requirements specification and formal methods. In particular, we propose a new specification language, called Formal Tropos, that is founded on the primitive concepts of early requirements frameworks (actor, goal, strategic dependency) [15], but supplements them with a rich temporal specification language. We also extend existing formal analysis techniques, in particular model checking, to allow for an automatic verification of relevant proper-ties for an early requirements specification. Our preliminary experiments demonstrate that formal analysis reveals gaps and inconsistencies in early requirements that are by no means trivial to discover without the help of formal analysis tools.

Cited By

View all

Karna AChen YYu HZhong HZhao J(2018)The role of model checking in software engineeringFrontiers of Computer Science: Selected Publications from Chinese Universities10.1007/s11704-016-6192-012:4(642-668)Online publication date: 1-Aug-2018
https://dl.acm.org/doi/10.1007/s11704-016-6192-0
Yadav NThangarajah J(2016)Checking the conformance of requirements in agent designs using ATLProceedings of the Twenty-second European Conference on Artificial Intelligence10.3233/978-1-61499-672-9-243(243-251)Online publication date: 29-Aug-2016
https://dl.acm.org/doi/10.3233/978-1-61499-672-9-243
Amato FMoscato F(2015)A model driven approach to data privacy verification in E-Health systemsTransactions on Data Privacy10.5555/2870503.28705068:3(273-296)Online publication date: 1-Dec-2015
https://dl.acm.org/doi/10.5555/2870503.2870506
Show More Cited By

Model Checking Early Requirements Specifications in Tropos
1. Software and its engineering
  1. Software creation and management
    1. Designing software
  2. Software organization and properties
    1. Software functional properties
      1. Formal methods

Recommendations

Specifying and analyzing early requirements in Tropos

We present a framework that supports the formal verification of early requirements specifications. The framework is based on Formal Tropos, a specification language that adopts primitive concepts for modeling early requirements (such as actor, goal, and ...
Consistency checking of SCR-style requirements specifications
RE '95: Proceedings of the Second IEEE International Symposium on Requirements Engineering

The paper describes a class of formal analysis called consistency checking that mechanically checks requirements specifications, expressed in the SCR tabular notation, for application independent properties. Properties include domain coverage, type ...
Analyzing tabular requirements specifications using infinite state model checking
MEMOCODE '06: Proceedings of the Fourth ACM/IEEE International Conference on Formal Methods and Models for Co-Design

This paper investigates the application of infinite state model checking to the formal analysis of requirements specifications in the SCR (software cost reduction) tabular notation using action language verifier (ALV). After reviewing the SCR method and ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

RE '01: Proceedings of the Fifth IEEE International Symposium on Requirements Engineering

August 2001

Publisher

IEEE Computer Society

United States

Publication History

Published: 27 August 2001

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

35
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 13 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Karna AChen YYu HZhong HZhao J(2018)The role of model checking in software engineeringFrontiers of Computer Science: Selected Publications from Chinese Universities10.1007/s11704-016-6192-012:4(642-668)Online publication date: 1-Aug-2018
https://dl.acm.org/doi/10.1007/s11704-016-6192-0
Yadav NThangarajah J(2016)Checking the conformance of requirements in agent designs using ATLProceedings of the Twenty-second European Conference on Artificial Intelligence10.3233/978-1-61499-672-9-243(243-251)Online publication date: 29-Aug-2016
https://dl.acm.org/doi/10.3233/978-1-61499-672-9-243
Amato FMoscato F(2015)A model driven approach to data privacy verification in E-Health systemsTransactions on Data Privacy10.5555/2870503.28705068:3(273-296)Online publication date: 1-Dec-2015
https://dl.acm.org/doi/10.5555/2870503.2870506
Abushark YThangarajah JMiller THarland JWinikoff MWeiss GYolum PBordini RElkind E(2015)Early Detection of Design Faults Relative to Requirement Specifications in Agent-Based ModelsProceedings of the 2015 International Conference on Autonomous Agents and Multiagent Systems10.5555/2772879.2773287(1071-1079)Online publication date: 4-May-2015
https://dl.acm.org/doi/10.5555/2772879.2773287
Abushark YThangarajah JMiller THarland JBazzan AHuhns MLomuscio AScerri P(2014)Checking consistency of agent designs against interaction protocols for early-phase defect locationProceedings of the 2014 international conference on Autonomous agents and multi-agent systems10.5555/2615731.2617395(933-940)Online publication date: 5-May-2014
https://dl.acm.org/doi/10.5555/2615731.2617395
Aceituna DDo HSrinivasan SJalote PBriand LHoek A(2014)A systematic approach to transforming system requirements into model checking specificationsCompanion Proceedings of the 36th International Conference on Software Engineering10.1145/2591062.2591183(165-174)Online publication date: 31-May-2014
https://dl.acm.org/doi/10.1145/2591062.2591183
Degiovanni RAlrajeh DAguirre NUchitel SJalote PBriand LHoek A(2014)Automated goal operationalisation based on interpolation and SAT solvingProceedings of the 36th International Conference on Software Engineering10.1145/2568225.2568323(129-139)Online publication date: 31-May-2014
https://dl.acm.org/doi/10.1145/2568225.2568323
Sabatucci LRibino PLodato CLopes33 SCossentino M(2013)GoalSPECProceedings of the First International Conference on Engineering Multi-Agent Systems10.5555/3100666.3100679(235-254)Online publication date: 6-May-2013
https://dl.acm.org/doi/10.5555/3100666.3100679
Dutta ABhattacharjee SKanjilal ADasgupta RBhattacharya S(2013)Engineering of requirements for a distributed teleteaching systemACM SIGSOFT Software Engineering Notes10.1145/2532780.253281438:6(1-12)Online publication date: 11-Nov-2013
https://dl.acm.org/doi/10.1145/2532780.2532814
Paja EDalpiaz FGiorgini P(2013)Managing Security Requirements Conflicts in Socio-Technical SystemsProceedings of the 32nd International Conference on Conceptual Modeling - Volume 821710.1007/978-3-642-41924-9_23(270-283)Online publication date: 11-Nov-2013
https://dl.acm.org/doi/10.1007/978-3-642-41924-9_23
Show More Cited By

Abstract

Cited By

Recommendations

Specifying and analyzing early requirements in Tropos

Consistency checking of SCR-style requirements specifications

Analyzing tabular requirements specifications using infinite state model checking

Comments

Information

Published In

Publisher

Publication History

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations