More Web Proxy on the site http://driver.im/

Article

A systematic approach to transforming system requirements into model checking specifications

Authors:

Daniel Aceituna,

Sudarshan SrinivasanAuthors Info & Claims

ICSE Companion 2014: Companion Proceedings of the 36th International Conference on Software Engineering

Pages 165 - 174

https://doi.org/10.1145/2591062.2591183

Published: 31 May 2014 Publication History

Abstract

We propose a method that addresses the following dilemma: model checking can formally expose off-nominal behaviors and unintended scenarios in the requirements of concurrent reactive systems. Requirements engineers and non-technical stakeholders who are the system domain experts can greatly benefit from jointly using model checking during the elicitation, analysis, and verification of system requirements. However, model checking is formal verification and many requirements engineers and domain experts typically lack the knowledge and training needed to apply model checking to the formal verification of requirements. To get full advantages of model checking and domain experts’ knowledge in verifying the system, we proposed a front end framework to model checking and evaluated our approach using a real world application.

References

[1]

D. Aceituna, H. Do, and S. Lee. Interactive requirements validation for reactive systems through virtual requirements prototype. In MoDRE, pages 1–10, 2011.

[2]

D. Aceituna, H. Do, G. Walia, and S. Lee. Evaluating the use of model-based requirements verification method: A feasibility study. In EmpiRE, pages 13–20, 2011.

[3]

J. Atlee and J. Gannon. State-based model checking of event-driven system requirements. TSE, 19:24–40, 1993.

Digital Library

[4]

A. Bierel, A. Cimatti, E. M. Clarke, O. Strichman, and Y. Zhu. Bounded model checking. Advances in Computers, 58:117–148, 2003.

[5]

B. Boehm. Anchoring the software process, 1995.

[6]

B. Boehm and V. Basili. Software defect reduction top 10 list. IEEE Computer, pages 135–137, 2001.

Digital Library

[7]

W. Chan, R. Anderson, P. Beame, S. Burns, F. Modugno, D. Notkin, and J. Reese. Model checking large software specifications. TSE, 24(7):156–166, 1998.

Digital Library

[8]

K. Cheung. Verify SCR requirements using XSPIN model checking to elevator case study, 2001.

[9]

Y. Choi and M. Heimdahl. Model checking RSML-e cequirements. In HASE, pages 109–118, 2002.

Digital Library

[10]

Y. Choi, S. Rayadurgam, and M. Heimdahl. Toward automation for model-checking requirements specifications with numeric constraints. RE, 7(4):225–242, 2002.

[11]

A. Cimatti, E. Clarke, F. Giunchiglia, and M. Roveri. NuSMV: A new symbolic model verifier. In CAV, pages 495–499, 1999.

Digital Library

[12]

E. Clarke, E. Emerson, and A. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. In TOPLAS, pages 244–263, 1986.

Digital Library

[13]

E. Clarke, O. Grumberg, and D. Peled. Model Checking. The MIT Press, first edition, 1999.

Digital Library

[14]

E. Clarke, O. Grumberg, H. Hiraishi, S. Jha, D. Long, K. McMillan, and L. Ness. Verification of the Futurebus+ Cache Coherence Protocol. FMSD, 6(2):217–232, 1995.

Digital Library

[15]

E. Clarke, D. Long, and K. Mcmillan. Compositional model checking. MIT Press, 1999.

Digital Library

[16]

M. Dwyer, G. Avrunin, and J. Corbett. Property specification patterns for finite-state verification. In FMSP, pages 7–15, 1998.

Digital Library

[17]

M. Dwyer, G. Avrunin, and J. Corbett. Patterns in property specifications for finite-state verification. In ICSE, pages 411–420, 1999.

Digital Library

[18]

A. Fantechi, S. Gnesi, G. Ristori, M. Carenini, M. Vanocchi, and P. Moreschini. Assisting requirement formalization by means of natural language translation. FMSD, 4(3):243–263, 1994.

Digital Library

[19]

D. Foyle and B. Hooey. Improving evaluation and system design through the use of off-nominal testing: A methodology for scenario development. In Internaltional Symposium on Aviation Psychology, pages 397–402, 2003.

[20]

A. Fuxman, M. Pistore, J. Mylopoulos, and P. Traverso. Model checking early requirements specifications in tropos. In RE, pages 174–181, 2001.

Digital Library

[21]

M. Giese and R. Heldal. From informal to formal specifications in UML. In UML, pages 197–211.

[22]

C. Heitmeyer, J. Kirby, B. Labaw, M. Archer, and R. Bharadwaj. Using abstraction and model checking to detect safety violations in requirements specifications. TSE, 24(11):927–948, 1998.

Digital Library

[23]

S. Konrad and B. Cheng. Facilitating the construction of specification pattern-based properties. In RE, pages 329–338, 2005.

Digital Library

[24]

A. Lamsweerde. Formal specification: a roadmap. In ICSE, pages 147–159, 2000.

Digital Library

[25]

N. Leveson. The role of software in recent aerospace accidents. In International System Safety Conference, 2001.

[26]

N. Leveson. Systemic factors in software-related spacecraft accidents, 2001.

[27]

S. Mallick and S. Krishna. Requirements engineering: Problem domain knowledge capture and the deliberation process support. In DEXA, pages 392–397, 1999.

Digital Library

[28]

B. Nuseibeh and S. Easterbrook. Requirements engineering: a roadmap. In ICSE, pages 35–46, 2000.

Digital Library

[29]

T. Sreemani and J. Atlee. Feasibility of model checking software requirements: A case study. In Computer Assurance, pages 77–88, 1996.

[30]

U. Stern and D. Dill. Automatic verification of the SCI cache coherence protocol. In IFIP WG10.5, pages 21–34, 1995.

Digital Library

[31]

K. Suda and N. Rani. The importance of risk radar in software risk management: A case of a Malaysian company. J. of Business and Social Science, 1(3), 2010.

[32]

N. Ubayashi, Y. Kamei, M. Hirayama, and T. Tamai. A context analysis method for embedded systems - Exploring a requirement boundary between a system and its context. In RE, pages 143–152, 2011.

Digital Library

[33]

C. Wang, Z. Yang, V. Kahlon, and A. Gupta. Peephole partial order reduction. In TACAS, pages 382–396, 2008.

Digital Library

[34]

E. Yu. Social modeling and i. In Conceptual Modeling: Foundations and Applications, pages 99–121, 2009.

Digital Library

Cited By

Leite GArruda FAntonino PSampaio ARoscoe A(2024)Extracting Formal Smart-Contract Specifications from Natural Language with LLMsFormal Aspects of Component Software10.1007/978-3-031-71261-6_7(109-126)Online publication date: 9-Sep-2024
https://dl.acm.org/doi/10.1007/978-3-031-71261-6_7
Nardone VSantone ATipaldi MLiuzza DGlielmo L(2019)Model Checking Techniques Applied to Satellite Operational Mode ManagementIEEE Systems Journal10.1109/JSYST.2018.279366513:1(1018-1029)Online publication date: Mar-2019
https://doi.org/10.1109/JSYST.2018.2793665
Aceituna DDo H(2019)Addressing the state explosion problem when visualizing off-nominal behaviors in a set of reactive requirementsRequirements Engineering10.1007/s00766-017-0281-y24:2(161-180)Online publication date: 17-May-2019
https://dl.acm.org/doi/10.1007/s00766-017-0281-y
Show More Cited By

Index Terms

A systematic approach to transforming system requirements into model checking specifications
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Software defect analysis
        Software testing and debugging

Recommendations

Model Checking Complete Requirements Specifications Using Abstraction

Although model checking has proven remarkably effective in detecting errors in hardware designs, its success in the analysis of software specifications has been limited. Model checking algorithms for hardware verification commonly use Binary Decision ...
Model Checking Process with Goal Oriented Requirements Analysis
APSEC '08: Proceedings of the 2008 15th Asia-Pacific Software Engineering Conference

Model checking is a powerful technique for verifying the correctness of a system’s specification. But even when the specification has been verified to be correct, there is still the question of whether the specification covers all the expected ...
Model-based requirements verification method

ContextRequirements engineering is one of the most important and critical phases in the software development life cycle, and should be carefully performed to build high quality and reliable software. However, requirements are typically gathered through ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ICSE Companion 2014: Companion Proceedings of the 36th International Conference on Software Engineering

May 2014

741 pages

ISBN:9781450327688

DOI:10.1145/2591062

General Chair:
Pankaj Jalote
IIIT-Delhi, India
,
Program Chairs:
Lionel Briand
University of Luxembourg, Luxembourg
,
André van der Hoek
University of California, Irvine, USA

Copyright © 2014 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGSOFT: ACM Special Interest Group on Software Engineering

In-Cooperation

TCSE: IEEE Computer Society's Tech. Council on Software Engin.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 31 May 2014

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

ICSE '14

Sponsor:

SIGSOFT

ICSE '14: 36th International Conference on Software Engineering

May 31 - June 7, 2014

Hyderabad, India

Acceptance Rates

Overall Acceptance Rate 276 of 1,856 submissions, 15%

Upcoming Conference

ICSE 2025

2025 IEEE/ACM 46th International Conference on Software Engineering

April 26 - May 3, 2025

Ottawa , ON , Canada

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

10
Total Citations
View Citations
305
Total Downloads

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

Reflects downloads up to 13 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Leite GArruda FAntonino PSampaio ARoscoe A(2024)Extracting Formal Smart-Contract Specifications from Natural Language with LLMsFormal Aspects of Component Software10.1007/978-3-031-71261-6_7(109-126)Online publication date: 9-Sep-2024
https://dl.acm.org/doi/10.1007/978-3-031-71261-6_7
Nardone VSantone ATipaldi MLiuzza DGlielmo L(2019)Model Checking Techniques Applied to Satellite Operational Mode ManagementIEEE Systems Journal10.1109/JSYST.2018.279366513:1(1018-1029)Online publication date: Mar-2019
https://doi.org/10.1109/JSYST.2018.2793665
Aceituna DDo H(2019)Addressing the state explosion problem when visualizing off-nominal behaviors in a set of reactive requirementsRequirements Engineering10.1007/s00766-017-0281-y24:2(161-180)Online publication date: 17-May-2019
https://dl.acm.org/doi/10.1007/s00766-017-0281-y
Madala KGaither DNielsen RDo H(2017)Automated Identification of Component State Transition Model Elements from Requirements2017 IEEE 25th International Requirements Engineering Conference Workshops (REW)10.1109/REW.2017.73(386-392)Online publication date: Sep-2017
https://doi.org/10.1109/REW.2017.73
Filax MGonschorek TOrtmeier F(2017)Building Models We Can Rely On: Requirements Traceability for Model-Based Verification TechniquesModel-Based Safety and Assessment10.1007/978-3-319-64119-5_1(3-18)Online publication date: 2-Aug-2017
https://doi.org/10.1007/978-3-319-64119-5_1
Aceituna D(2016)Elicitation Practices That Can Decrease Vulnerability to Off-Nominal Behaviors: Lessons from using the Causal Component ModelSAE International Journal of Passenger Cars - Electronic and Electrical Systems10.4271/2016-01-810910:1Online publication date: 27-Sep-2016
https://doi.org/10.4271/2016-01-8109
Carvalho GCavalcanti ASampaio A(2016)Modelling timed reactive systems from natural-language requirementsFormal Aspects of Computing10.1007/s00165-016-0387-x28:5(725-765)Online publication date: 26-Jul-2016
https://doi.org/10.1007/s00165-016-0387-x
Barza SCarvalho GIyoda JSampaio AMota ABarros F(2016)Model Checking RequirementsFormal Methods: Foundations and Applications10.1007/978-3-319-49815-7_13(217-234)Online publication date: 13-Nov-2016
https://doi.org/10.1007/978-3-319-49815-7_13
Aceituna DDo H(2015)Exposing the susceptibility of off-nominal behaviors in reactive system requirements2015 IEEE 23rd International Requirements Engineering Conference (RE)10.1109/RE.2015.7320416(136-145)Online publication date: Aug-2015
https://doi.org/10.1109/RE.2015.7320416
Shchurov AMarik R(2015)A presentation format of architecture description based on the concept of multilayer networks2015 ITU Kaleidoscope: Trust in the Information Society (K-2015)10.1109/Kaleidoscope.2015.7383623(1-6)Online publication date: Dec-2015
https://doi.org/10.1109/Kaleidoscope.2015.7383623

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents