형식 사양

Formal specification

컴퓨터 과학에서 공식 사양은 시스템과 소프트웨어의 구현을 돕는 것을 목적으로 하는 수학 기반 기술입니다.이들은 시스템을 기술하고, 그 동작을 분석하며, 엄격하고 효과적인 추론 [1][2]도구를 통해 관심 있는 주요 특성을 검증함으로써 설계에 도움을 주기 위해 사용됩니다.이러한 사양은 구문을 가지며, 그 의미론은 하나의 영역에 속하며, 유용한 [3]정보를 추론하는 데 사용될 수 있다는 점에서 형식적이다.

동기

지난 10년 동안 컴퓨터 시스템은 점점 더 강력해졌고 그 결과 사회에 더 큰 영향을 미치고 있습니다.따라서 신뢰성 높은 소프트웨어의 설계와 구현을 지원하기 위해서는 보다 나은 기술이 필요합니다.확립된 엔지니어링 분야에서는 제품 설계를 만들고 검증하는 기초로서 수학적 분석을 사용합니다.정식 사양은 소프트웨어 엔지니어링의 신뢰성에서 이를 실현하기 위한 하나의 방법입니다.코드 [1]품질을 향상시키기 위해 테스트와 같은 다른 방법이 더 일반적으로 사용됩니다.

사용하다

이러한 사양에 따라 시스템 설계가 사양과 관련하여 올바르다는 것을 증명하기 위해 공식적인 검증 기법을 사용할 수 있습니다.이것에 의해, 실제의 실장에의 대규모 투자를 실시하기 전에, 잘못된 시스템 설계를 수정할 수 있습니다.또 다른 접근법은 아마도 정확한 개선 단계를 사용하여 사양을 설계로 변환하고, 최종적으로 구조에 의해 올바른 구현으로 변환하는 것입니다.

정식 사양은 구현이 아니라 구현 개발에 사용될 수 있다는 점에 유의해야 합니다.정식 사양은 시스템이 무엇을 해야 하는지를 기술하는 것이지 시스템이 어떻게 해야 하는지를 기술하는 것은 아닙니다.

적절한 사양은 적절한, 내부적으로 일관성 있는, 모호하지 않은, 완전함, 만족함, 최소의[3] 몇 가지 속성을 가져야 합니다.

적절한 사양은 [3]다음과 같습니다.

  • 구성성, 관리성 및 진화 가능성
  • 조작성
  • 통신성
  • 강력하고 효율적인 분석

정식 사양에 관심이 있는 주요 이유 중 하나는 소프트웨어 [2]구현에 대한 증명을 수행할 수 있는 능력을 제공하기 때문입니다.이러한 증명은 사양의 유효성 확인, 설계의 정확성 확인 또는 프로그램이 [2]사양을 충족한다는 것을 증명하기 위해 사용될 수 있다.

제한 사항

설계(또는 구현)는 그 자체로는 결코 "올바른" 것으로 선언할 수 없습니다."특정 사양에 관해서"만 정확할 수 있습니다.정식 사양이 해결해야 할 문제를 올바르게 기술하고 있는지 여부는 별개의 문제입니다.또한 그것은 궁극적으로 비공식적인 구체적인 문제 영역의 추상화된 공식 표현을 구성하는 문제와 관련이 있고, 그러한 추상화 단계는 공식적인 증거에 따를 수 없기 때문에 다루기가 어려운 문제이다.단, 사양이 제시될 것으로 예상되는 속성에 관한 "도전" 이론을 증명함으로써 사양을 검증할 수 있다.올바른 경우, 이러한 정리는 규격에 대한 지정자의 이해와 기본 문제 영역과의 관계를 강화합니다.그렇지 않은 경우, 규격을 작성(및 구현)하는 데 관련된 사람들의 도메인 이해를 더 잘 반영하도록 규격을 변경해야 할 수 있습니다.

정식 소프트웨어 개발 방법은 업계에서 널리 사용되지 않습니다.대부분의 기업은 소프트웨어 개발 [4]프로세스에 적용하는 것이 비용 효율적이라고 생각하지 않습니다.여기에는 다음과 같은 다양한 이유가 있을 수 있습니다.

  • 시간을
    • 높은 초기 시작 비용과 낮은 수익률
  • 유연성
    • 많은 소프트웨어 기업이 유연성에 중점을 둔 민첩한 방법을 사용하고 있습니다.시스템 전체의 정식 사양을 사전에 실행하는 것은 유연성의 반대로 인식되는 경우가 많습니다.다만, 「신속한」개발에[5] 정식 사양을 사용하는 것의 이점에 대해서는, 몇개의 연구가 있다.
  • 복잡성
    • 이를 효과적으로[5] 이해하고 적용하기 위해서는 높은 수준의 수학적 전문지식과 분석능력이 필요합니다.
    • 이에 대한 해결책은 이러한 기술을 구현할 수 있도록 허용하지만 기본 수학을[2][5] 숨기는 도구와 모델을 개발하는 것입니다.
  • 한정된[3] 범위
    • 프로젝트의[3] 모든 이해관계자가 관심을 갖는 속성을 캡처하는 것은 아닙니다.
    • 사용자 인터페이스와 사용자 상호[4] 작용을 제대로 지정하지 못합니다.
  • 비용 효율이 낮다
    • 이는 비용[4] 효율이 뛰어난 것으로 판명된 중요한 시스템의 핵심 부품에만 사용을 제한함으로써 완전히 사실이 아닙니다.

기타 제한 사항:[3]

  • 격리
  • 저레벨 온톨로지
  • 안내가 불충분하다
  • 우려의 분리가 불충분
  • 툴 피드백 부족

패러다임

정식 사양 기술은 오랜 [6]기간 동안 다양한 영역과 다양한 규모로 존재해 왔습니다.정식 사양의 실장은, 모델화하는 시스템의 종류, 적용 방법, 및 소프트웨어 라이프 사이클의 어느 시점에서 [2]도입되었는지에 따라서 다릅니다.이러한 유형의 모형은 다음과 같은 규격 패러다임으로 분류할 수 있습니다.

  • 이력 기반 사양[3]
    • 시스템 이력에 근거한 동작
    • 주장은 시간이 지남에 따라 해석된다
  • 상태 기반 사양[3]
    • 시스템 상태에 따른 동작
    • 일련의 순차적 단계(예: 금융 거래)
    • Z, VDM, B 등의 언어는 이 패러다임에[3] 의존합니다.
  • 전환 기반 사양[3]
    • 시스템 상태에서 상태로의 이행에 근거한 동작
    • 반응성 시스템과 함께 가장 잘 사용됨
    • StateCharts, PROMELA, STeP-SPL, RSML, SCR 등의 언어는 이 패러다임에[3] 의존합니다.
  • 기능사양서[3]
    • 수학 함수의 구조로서 시스템을 지정하다
    • OBJ, ASL, PLUSS, LARCH, HOL 또는 PVS는 이 패러다임에[3] 의존합니다.
  • 운용사양서[3]
    • 페이즐리, GIST, 페트리 네트 또는 프로세스 대수와 같은[3] 초기 언어들은 이 패러다임에 의존한다.

상기 패러다임 외에 특정 휴리스틱스를 적용하여 이들 사양의 작성을 개선하는 방법도 있습니다.여기서 참조하는 논문은 사양을 [6]설계할 때 사용하는 휴리스틱스에 대해 가장 잘 설명합니다.이들은 분할 및 정복 방식을 적용하여 이를 수행합니다.

소프트웨어 도구

Z 표기법은 대표적인 형식 사양 언어의 예입니다.Vienna Development Method의 Specification Language(VDM-SL)와 B-Method의 Abstract Machine Notation(AMN; 추상 기계 표기법)이 있습니다.Web 서비스 영역에서는 기능하지 않는 속성[7](Web 서비스 품질)을 기술하기 위해 정식 사양이 자주 사용됩니다.

툴에는 다음과 같은 것이 있습니다.[4]

예

구현 예는 소프트웨어 도구 섹션의 링크를 참조하십시오.

「 」를 참조해 주세요.

레퍼런스

  1. ^ a b Hierons, R. M.; Bogdanov, K.; Bowen, J. P.; Cleaveland, R.; Derrick, J.; Dick, J.; Gheorghe, M.; Harman, M.; Kapoor, K.; Krause, P.; Lüttgen, G.; Simons, A. J. H.; Vilkomir, S. A.; Woodward, M. R.; Zedan, H. (2009). "Using formal specifications to support testing". ACM Computing Surveys. 41 (2): 1. CiteSeerX 10.1.1.144.3320. doi:10.1145/1459352.1459354. S2CID 10686134.
  2. ^ a b c d e Gaudel, M.-C. (1994). "Formal specification techniques". Proceedings of 16th International Conference on Software Engineering. pp. 223–227. doi:10.1109/ICSE.1994.296781. ISBN 978-0-8186-5855-6. S2CID 60740848.
  3. ^ a b c d e f g h i j k l m n o Lamsweerde, A. V. (2000). "Formal specification". Proceedings of the conference on the future of Software engineering - ICSE '00. pp. 147–159. doi:10.1145/336512.336546. ISBN 978-1581132533. S2CID 4657483.
  4. ^ a b c d Sommerville, Ian (2009). "Formal Specification" (PDF). Software Engineering. Retrieved 3 February 2013.
  5. ^ a b c Nummenmaa, Timo; Tiensuu, Aleksi; Berki, Eleni; Mikkonen, Tommi; Kuittinen, Jussi; Kultima, Annakaisa (4 August 2011). "Supporting agile development by facilitating natural user interaction with executable formal specifications". ACM SIGSOFT Software Engineering Notes. 36 (4): 1–10. doi:10.1145/1988997.2003643. S2CID 2139235.
  6. ^ a b van der Poll, John A.; Paula Kotze (2002). "What design heuristics may enhance the utility of a formal specification?". Proceedings of the 2002 Annual Research Conference of the South African Institute of Computer Scientists and Information Technologists on Enablement Through Technology. SAICSIT '02: 179–194. ISBN 9781581135961.
  7. ^ S-Cube 지식 모델:정식 사양

외부 링크

Wikimedia Commons에는 정식 사양과 관련된 미디어가 있습니다.