Formalna weryfikacja wymagań systemów czasu rzeczywistego

Abstract

The methodology of system requirements verification presented in this paper is a proposition of a practical procedure for reducing some negatives of the specification of requirements. The main problem that is considered is to create a complete description of the system requirements without any negatives. Verification of the initially defined requirements is based on the coloured Petri nets. Those nets are useful for testing some properties of system requirements such as completeness, consistency and optimality. An example of the lift controller is presented. W artykule przedstawiono zagadnienia związane z pierwszą fazą tworzenia modeli systemów czasu rzeczywistego, tzn. fazą analizy wymagań. Przedmiotem szczególnego zainteresowania jest tworzenie pełnego i niesprzecznego opisu wymaganego zachowania się modelowanego systemu. Weryfikacja wstępnie sformułowanych wymagań dokonuje się z wykorzystaniem kolorowanych sieci Petriego. Wybór ten uwarunkowany jest łatwym dostępem do komputerowych narzędzi, które pozwalają w szybki sposób konstruować i analizować takie sieci. Efektem tak przeprowadzonej weryfikacji jest kompletny, pozbawiony sprzeczności opis wymagań systemu, dotyczących jego obserwowalnego z zewnątrz zachowania. Rozważania zamieszczone poniżej są ilustrowane przykładem sterownika windy.