소프트웨어 모델 검사에 대한 경험은 무엇입니까?[닫은]
https://stackoverflow.com/questions/25137
-
09-06-2019 - |
italiano
english
français
española
中国
日本の
العربية
Deutsch
한국어
Português
Russian문제
- 어떤 유형의 애플리케이션에 모델 검사 를 사용 했습니까?
- 어떤 모델 확인 도구를 사용하셨습니까?
- 기술에 대한 경험, 특히 고품질 소프트웨어를 제공하는 데있어 그 효과를 평가 한 경험을 어떻게 요약 하시겠습니까?
연구 과정에서 Spin 을 사용할 기회가 있었는데실제 모델 검사가 얼마나 진행되고 있으며 조직이 얼마나 많은 가치를 얻고 있는지 궁금합니다.제 업무 경험에서 저는 논리에 공식적인 검증을 적용하는 것에 대해 (당연히) 고려할 필요가없는 비즈니스 애플리케이션을 작업했습니다.나는 주제에 대한 경험과 생각을 확인하는 SO 사람들 모델에 대해 정말로 배우고 싶습니다.모델 검사가 툴킷에서 가져야하는 개발 방식이 더 널리 사용됩니까?
해결책
저는 방금 모델 검사에 대한 수업을 마쳤으며 우리가 사용한 큰 도구는 Spin 이고 SMV . 우리는 그것들을 사용하여 일반적인 동기화 문제에 대한 속성을 확인했고 SMV를 사용하기가 조금 더 쉽다는 것을 알았습니다.
이 도구는 사용하기 재미 있었지만 프로그램에 대한 제약을 동적으로 적용하는 도구와 결합 할 때 정말 빛난다 고 생각합니다 (프로그램에 대한 '유용한'사항을 확인하는 것이 조금 더 쉽습니다). 결국 우리는 Spring WebFlow 프레임 워크 를 사용했습니다.이 프레임 워크는 XML을 사용하여 다음을 지정하는 상태 시스템과 같은 파일을 작성합니다. 다른 웹 페이지로 전환 할 수있는 웹 페이지 및 SMV를 사용하여 해당 응용 프로그램에서 확인을 수행 할 수 있습니다 ( 여기에 뻔뻔한 플러그 ).
마지막 질문에 답하기 위해 모델 검사가 확실히 유용하다고 생각하지만, 최종 제품을 제공하는 데 편안함을 느끼게하는 기법으로 단위 테스트를 사용하는 것이 더 좋습니다.
다른 팁
우리는 교육, 시스템 설계 및 시스템 개발에 여러 모델 검사기를 사용했습니다.우리의 도구 상자에는 SPIN, UPPAL, Java Pathfinder, PVS 및 Bogor가 포함됩니다.각각의 장점과 단점이 있습니다.모두 인간이 발견하기 불가능한 모델로 문제를 발견합니다.사용성은 다양하지만 대부분은 푸시 버튼이 자동화되어 있습니다.
모델 검사기는 언제 사용하나요?특정 속성이 있거나 없어야하는 모델을 설명 할 때마다 몇 가지 개념보다 더 큽니다.더 크거나 복잡한 것을 설명하고 이해할 수 있다고 생각하는 사람은 자신을 속이고 있습니다.
모델 검사를 사용한 애플리케이션 유형은 무엇입니까?
저희는 Java Path Finder 모델 검사기를 사용하여 일부 보안 (교착 상태, 경쟁 조건) 및 시간 속성 (선형 시간 논리를 사용하여 지정)을 확인했습니다. Java (바이트 코드)에서 NotNull과 같은 고전적인 주장을 지원합니다.-프로그램 모델 검사를위한 것입니다. <인용구>
어떤 모델 확인 도구를 사용하셨습니까?
우리는 Java Path Finder 를 사용했습니다 (학술 용). NASA에서 처음 개발 한 오픈 소스 소프트웨어입니다. <인용구>
기술에 대한 경험, 특히 고품질 소프트웨어를 제공하는 데있어 그 효과를 평가하는 방법을 어떻게 요약 하시겠습니까?
프로그램 모델 검사는 상태 공간 폭발 (메모리 및 디스크 사용)과 관련된 주요 문제가 있습니다. 그러나 문제를 줄이고 부분적인 순서 감소, 추상화, 대칭 감소 등과 같은 큰 아티팩트를 처리하기위한 다양한 기술이 있습니다.
SPIN을 사용하여 PLC 소프트웨어에서 동시성 문제를 찾았습니다.검사 나 테스트로 찾기가 매우 어려웠을 의심하지 않는 경쟁 조건을 발견했습니다.
그런데 '스핀 for Dummies'책이 있나요?"The SPIN Model Checker"책과 다양한 온라인 튜토리얼에서 배워야했습니다.
대학 재학 기간 동안이 주제에 대한 조사를 수행하여 국가 탐사어셈블리 모델 검사기 .
우리는 가상 머신을 사용하여 오류의 종류 (교착 상태, I / O 오류 등)에 따라 A * 및 일부 휴리스틱을 사용하여 프로그램의 가능한 모든 경로 / 상태를 탐색했습니다.
Java Pathfinder 에서 영감을 얻었으며 C ++ 코드로 작동했습니다.(GCC가 컴파일 할 수있는 모든 것)
그러나 경험상 이러한 종류의 기술은 GUI 관련 문제, 초기 테스트 환경을 만드는 데 필요한 작업 및 엄청난 하드웨어 요구 사항으로 인해 곧 비즈니스 응용 프로그램에 사용되지 않을 것입니다.(거대한 상태 공간 때문에 많은 RAM과 디스크 공간이 필요합니다.)
