Verifying security requirements using model checking technique for UML-based requirements specification

Yoshitaka Aoki, Saeko Matsuura

Research output: Chapter in Book/Report/Conference proceedingConference contribution

5 Citations (Scopus)

Abstract

Use case analysis is known to be an effective method to clarify functional requirements. Security requirements such as access or information control tend to increase the complexity of functional requirements, and therefore, need to be correctly implemented to minimize risks. However, general developers find it difficult to correctly specify adequate security requirements during the initial phases of the software development process. We propose a method to verify security requirements whose specifications are based on Unified Modeling Language (UML) using the model checking technique and Common Criteria security knowledge. Common Criteria assists in defining adequate security requirements in the form of a table. This helps developers verify whether UML-based requirements analysis models meet those requirements in the early stages of software development. The UML model and the table are transformed into a finite automaton in the UPPAAL model checking tool.

Original languageEnglish
Title of host publication2014 IEEE 1st International Workshop on Requirements Engineering and Testing, RET 2014 - Proceedings
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages18-25
Number of pages8
ISBN (Print)9781479963348
DOIs
Publication statusPublished - 2014 Sep 23
Event2014 IEEE 1st International Workshop on Requirements Engineering and Testing, RET 2014 - Karlskrona
Duration: 2014 Aug 262014 Aug 26

Other

Other2014 IEEE 1st International Workshop on Requirements Engineering and Testing, RET 2014
CityKarlskrona
Period14/8/2614/8/26

Fingerprint

Unified Modeling Language
Model checking
Specifications
Software engineering
Finite automata
Requirements specification
Unified modeling language

Keywords

  • Access Control
  • Common Criteria
  • Model Checking
  • Security Requirements
  • UML
  • Verification

ASJC Scopus subject areas

  • Information Systems and Management
  • Software

Cite this

Aoki, Y., & Matsuura, S. (2014). Verifying security requirements using model checking technique for UML-based requirements specification. In 2014 IEEE 1st International Workshop on Requirements Engineering and Testing, RET 2014 - Proceedings (pp. 18-25). [6908674] Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/RET.2014.6908674

Verifying security requirements using model checking technique for UML-based requirements specification. / Aoki, Yoshitaka; Matsuura, Saeko.

2014 IEEE 1st International Workshop on Requirements Engineering and Testing, RET 2014 - Proceedings. Institute of Electrical and Electronics Engineers Inc., 2014. p. 18-25 6908674.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Aoki, Y & Matsuura, S 2014, Verifying security requirements using model checking technique for UML-based requirements specification. in 2014 IEEE 1st International Workshop on Requirements Engineering and Testing, RET 2014 - Proceedings., 6908674, Institute of Electrical and Electronics Engineers Inc., pp. 18-25, 2014 IEEE 1st International Workshop on Requirements Engineering and Testing, RET 2014, Karlskrona, 14/8/26. https://doi.org/10.1109/RET.2014.6908674
Aoki Y, Matsuura S. Verifying security requirements using model checking technique for UML-based requirements specification. In 2014 IEEE 1st International Workshop on Requirements Engineering and Testing, RET 2014 - Proceedings. Institute of Electrical and Electronics Engineers Inc. 2014. p. 18-25. 6908674 https://doi.org/10.1109/RET.2014.6908674
Aoki, Yoshitaka ; Matsuura, Saeko. / Verifying security requirements using model checking technique for UML-based requirements specification. 2014 IEEE 1st International Workshop on Requirements Engineering and Testing, RET 2014 - Proceedings. Institute of Electrical and Electronics Engineers Inc., 2014. pp. 18-25
@inproceedings{c20fbb67707c4f44902f6292c6caafb4,
title = "Verifying security requirements using model checking technique for UML-based requirements specification",
abstract = "Use case analysis is known to be an effective method to clarify functional requirements. Security requirements such as access or information control tend to increase the complexity of functional requirements, and therefore, need to be correctly implemented to minimize risks. However, general developers find it difficult to correctly specify adequate security requirements during the initial phases of the software development process. We propose a method to verify security requirements whose specifications are based on Unified Modeling Language (UML) using the model checking technique and Common Criteria security knowledge. Common Criteria assists in defining adequate security requirements in the form of a table. This helps developers verify whether UML-based requirements analysis models meet those requirements in the early stages of software development. The UML model and the table are transformed into a finite automaton in the UPPAAL model checking tool.",
keywords = "Access Control, Common Criteria, Model Checking, Security Requirements, UML, Verification",
author = "Yoshitaka Aoki and Saeko Matsuura",
year = "2014",
month = "9",
day = "23",
doi = "10.1109/RET.2014.6908674",
language = "English",
isbn = "9781479963348",
pages = "18--25",
booktitle = "2014 IEEE 1st International Workshop on Requirements Engineering and Testing, RET 2014 - Proceedings",
publisher = "Institute of Electrical and Electronics Engineers Inc.",

}

TY - GEN

T1 - Verifying security requirements using model checking technique for UML-based requirements specification

AU - Aoki, Yoshitaka

AU - Matsuura, Saeko

PY - 2014/9/23

Y1 - 2014/9/23

N2 - Use case analysis is known to be an effective method to clarify functional requirements. Security requirements such as access or information control tend to increase the complexity of functional requirements, and therefore, need to be correctly implemented to minimize risks. However, general developers find it difficult to correctly specify adequate security requirements during the initial phases of the software development process. We propose a method to verify security requirements whose specifications are based on Unified Modeling Language (UML) using the model checking technique and Common Criteria security knowledge. Common Criteria assists in defining adequate security requirements in the form of a table. This helps developers verify whether UML-based requirements analysis models meet those requirements in the early stages of software development. The UML model and the table are transformed into a finite automaton in the UPPAAL model checking tool.

AB - Use case analysis is known to be an effective method to clarify functional requirements. Security requirements such as access or information control tend to increase the complexity of functional requirements, and therefore, need to be correctly implemented to minimize risks. However, general developers find it difficult to correctly specify adequate security requirements during the initial phases of the software development process. We propose a method to verify security requirements whose specifications are based on Unified Modeling Language (UML) using the model checking technique and Common Criteria security knowledge. Common Criteria assists in defining adequate security requirements in the form of a table. This helps developers verify whether UML-based requirements analysis models meet those requirements in the early stages of software development. The UML model and the table are transformed into a finite automaton in the UPPAAL model checking tool.

KW - Access Control

KW - Common Criteria

KW - Model Checking

KW - Security Requirements

KW - UML

KW - Verification

UR - http://www.scopus.com/inward/record.url?scp=84908637078&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84908637078&partnerID=8YFLogxK

U2 - 10.1109/RET.2014.6908674

DO - 10.1109/RET.2014.6908674

M3 - Conference contribution

AN - SCOPUS:84908637078

SN - 9781479963348

SP - 18

EP - 25

BT - 2014 IEEE 1st International Workshop on Requirements Engineering and Testing, RET 2014 - Proceedings

PB - Institute of Electrical and Electronics Engineers Inc.

ER -