The problem o fieldbus protocol formal specification is characterized. Two techniques of time elapsing are indicated. Explicit specification of time constraints is described. Verification of a system that uses the specified protocol is carried out by means of tests, LOTOS specification language and its RT-LOTOS real time extension is used. Considerations are illustrated by simple example of Master-Slave protocol employed for vertical communication in small distributed system.%Scharakteryzowano problem formalnego specyfikowania protokołów komunikacyjnych dla magistral polowych. Wskazano dwa sposoby uwzględniania upływu czasu oraz omówiono zagadnienie jawnego specyfikowania ograniczeń czasowych komunikacji. Weryfikacje, poprawności systemu ze specyfi kowanym protokołem ograniczono do testów. Zastosowano język specyfikacji LOTOS oraz jego czasowe rozszerzenie RT-LOTOS. Rozważania zilustrowano prostym przykładem protokołu Master-Slave, powszechnie stosowanym w małych systemach rozproszonych.
展开▼
