mgr inĪ. Jan Sadolewski
Politechnika Rzeszowska, Katedra Informatyki i Automatyki
ASERCYJNE ROZSZERZENIE JĉZYKA ST NORMY IEC 61131-3
DO DYNAMICZNEJ WERYFIKACJI SYSTEMÓW STEROWANIA
1W pracy przedstawiono propozycjĊ asercyjnego rozszerzenia jĊzyka ST (Structu-red Text) normy IEC 61131-3, nawiązującego do reguá projektowania kontrakto-wego i jĊzyka JML (Java Modeling Language). Zapisane asercje moĪna prze-ksztaáciü do kodu podczas kompilacji w celu uzyskania moĪliwoĞci dynamicznej weryfikacji programów sterowania oraz detekcji báĊdów czujników. Przykáady do-tyczą sterowania ukáadem grzaáek w zaleĪnoĞci od temperatury oraz urządzenia do sortowania drewna.
ASSERTIONAL EXTENSION IN ST LANGUAGE OF IEC 61131-3 STANDARD FOR CONTROL SYSTEMS DYNAMIC VERIFICATION The paper presents a proposition of assertional extension in Structured Text lan-guage from IEC 61131-3 standard, according to design by contract rules and JML (Java Modeling Language). Stored assertions could be converted to the code at compile time to obtain possibility of dynamic verification and for sensors fail-ure detection. Heater control system and wood sorter machine are examples. 1. WPROWADZENIE
Wspóáczesne standardy tworzenia oprogramowania, wykorzystują projektowanie kontraktowe [7] (ang. design by contract). Zaletą takiego podejĞcia jest precyzyjne ustalenie zakresu fun-kcjonalnoĞci pomiĊdzy autorem specyfikacji warunków koĔcowych, a autorem implementacji i specyfikacji warunków początkowych. Ustalenia te nazywa siĊ kontraktem, który powinien zostaü zapisany w sposób formalny w pobliĪu kodu, który opisuje. JĊzyki programowania takie jak ANSI C, C++ czy Java mają wáasne narzĊdzia do formalnego zapisu specyfikacji (kontraktu) w postaci jĊzyków ACSL, Larch, i JML [1, 5, 6], ponadto jĊzyki Eiffel i Why [8, 3] mają wbudowaną w skáadniĊ moĪliwoĞü zapisania specyfikacji bezpoĞrednio w ich kodzie. Tak zapisaną specyfikacjĊ moĪna poddaü weryfikacji statycznej z jej implementacją w celu wychwycenia i usuniĊcia báĊdów w implementacji oraz do przedstawienia formalnego dowo-du zgodnoĞci. Niniejsza praca przedstawia propozycjĊ asercyjnego rozszerzenia jĊzyka ST normy IEC 61131-3 do programowania systemów sterowania. Rozszerzenie to oparto na standardzie JML, wprowadzając jednoczeĞnie moĪliwoĞü weryfikacji dynamicznej programu w czasie jego wykonywania (run-time checking), a takĪe podjĊcia akcji ratunkowej w sytuacjach nie speániających zaáoĪonego kryterium.
Praca podzielona jest nastĊpująco. W punkcie 2 omówiono cechy i zastosowanie asercji w jĊzykach programowania w tym standardu JML. Punkt 3 zawiera semantykĊ asercyjnego rozszerzenia jĊzyka ST oraz jego uzupeánienie do obsáugi sytuacji krytycznych. Punkt 4 opi-suje znaczenie klauzul podczas weryfikacji dynamicznej. W punkcie 5 przedstawiono dwa proste przykáady systemów sterowania wykorzystujące asercyjne rozszerzenie do weryfikacji dynamicznej oraz wykrywania defektów czujników.
1
Praca naukowa finansowana ze Ğrodków na naukĊ w latach 2010 – 2011 jako projekt badawczy nr N N516 41538.
2. ASERCJE W JĉZYKACH PROGRAMOWANIA
Asercją nazywamy fragment kodu skáadającego siĊ z co najmniej wyraĪenia logicznego, któ-rego kaĪdorazowe obliczenie w miejscu i kolejnoĞci jego wstąpienia ma zwróciü wartoĞü po-zytywną. Standardowe asercje w jĊzykach programowania takich jak ANSI C, Delphi (Pas-cal), czy C# przedstawiono w tab. 1. Typowo mają zastosowanie tylko do celów testowych, a ich kod „znika” w czasie kompilacji do postaci finalnej opracowywanego moduáu. Po zmia-nie odpowiednich ustawieĔ w kompilatorze postaü finalna moĪe rówzmia-nieĪ zawieraü asercje. Problem pojawia siĊ dopiero w sytuacjach, kiedy sprawdzenie warunku asercji zwraca war-toĞü negatywną. W zaleĪnoĞci od implementacji niespeánienie asercji koĔczy siĊ oknem ko-munikatu, utworzeniem wyjątku, bądĨ przerwaniem programu. Drugim utrudnieniem przy korzystaniu ze standardowych asercji są komunikaty pomocnicze, w najlepszym przypadku definiowane przez uĪytkownika, w których nie ma informacji o przyczynach ich niespeánie-nia. Projektowanie kontraktowe wykorzystuje dwie dodatkowe asercje requires do
okreĞle-nia warunków wstĊpnych i ensures do warunków koĔcowych projektowanej, a nastĊpnie
formalnie weryfikowanej jednostki. Asercje te zapisywane są w postaci adnotacji do kodu poprzez odpowiednie klauzule jĊzyka lub komentarze specjalne. JĊzyki Eiffel i Why wyko-rzystują wbudowane klauzule, natomiast JML i ACSL uĪywają komentarzy rozpoczynających siĊ od znaku ‘@’. Ta cecha przyczyniáa siĊ do powstania standardu dla jĊzyków okreĞlanych
mianem BISL (Behavioral Interface Specification, Language), których przykáad stanowi standard JML. Wykorzystanie komentarzy jako miejsca do adnotacji pozwala na zapewnienie przenaszalnoĞci kodu Ĩródáowego pomiĊdzy kompilatorami róĪnych producentów.
Tab. 1. Asercje w popularnych jĊzykach programowania
ANSI C, POSIX Delphi, Pascal C# (Platforma .NET)
#include <assert.h> void additem(struct ITEM
*itemptr) { assert(itemptr != NULL); ... } procedure ModifyStorage (AStorage: TStorage;
const s: string); begin
Assert(AStorage <> nil, ''); AStorage.Data := s; end; { int index; ... System.Diagnostics.Debug .Assert(index > -1); ... }
Standard JML zawiera notacjĊ do zapisu formalnej specyfikacji zachowania klas i metod jĊ-zyka Java. ZuboĪone obiekty jĊjĊ-zyka Java przypominają jednostki oprogramowania (POU) zdefiniowane w normie 61131-3, dlatego wykorzystanie JML jako bazy dla asercyjnego roz-szerzenia jĊzyka ST wydaje siĊ uzasadnione. Naturalnym wydaje siĊ fakt, Īe tylko pewien podzbiór standardu JML bĊdzie miaá zastosowanie w systemach sterowania, dlatego aspekty typowe dla Java, nie mające odzwierciedlenia w ST, zostaáy pominiĊte.
3. SEMANTYKA ASERCYJNEGO ROZSZERZENIA JĉZYKA ST
AdaptacjĊ asercyjnego rozszerzenia dla jĊzyka ST przedstawiono w tab. 2. Klauzule jĊzyka zostaáy pogrupowane ze wzglĊdu na ich typ. KaĪda z klauzul ma zakres swojej widocznoĞci. Zakres instrukcji moĪe pojawiü siĊ w dowolnym miejscu programu, gdzie mogą znaleĨü siĊ instrukcje lub wyraĪenia. Zakres lokalny odnosi siĊ do caáej instancji obiektu POU, natomiast zakres globalny dotyczy caáego projektu (konfiguracji wg normy). Zakres mieszany sygnali-zuje moĪliwoĞü wystąpienia klauzuli w zaleĪnoĞci od kontekstu.
Z powodu konfliktów sáów kluczowych asercyjnego rozszerzenia z identyfikatorami jĊzyka ST, a takĪe w celu uáatwienia analizy kodu przez programistów, wprowadzono nastĊpujące nieznaczne modyfikacje:
– przeniesiono adnotacje opisujące zachowanie metody do wnĊtrza obiektu POU,
bezpo-Ğrednio po nazwie obiektu wystĊpującej w jego definicji2
,
– wprowadzono jednowierszowe komentarze w specyfikacji od znaków ‘//’ do
najbliĪsze-go znaku koĔca linii lub znaków ‘*)’ zamykających adnotacjĊ,
– wprowadzono znak dwukropka po sáowie kluczowym adnotacji rozpoczynającym
klau-zule i Ğrednik po wyraĪeniu wystĊpującym jako argument klauzuli.
Klauzule umieszcza siĊ wewnątrz opisywanej jednostki, z uwzglĊdnieniem jej zakresu wi-docznoĞci. Przeznaczeniem lokalnej klauzuli ensures jest wyraĪenie warunku koĔcowego
jednostki oprogramowania, jaki musi zostaü speániony po jej zakoĔczeniu wykonywania. Za-kres widocznoĞci tej klauzuli odnosi siĊ do jednostki, w której zostaáa zadeklarowana. Podob-nie klauzula requires wyraĪa warunki początkowe, jakie muszą zostaü speánione, aby
jed-nostka wykonaáa siĊ poprawnie przy speánionych warunkach początkowych, a otrzymany rezultat dziaáaĔ speániaá warunki koĔcowe tej jednostki. Klauzula assert sáuĪy do definicji
warunku, który powinien zostaü speániony w dowolnym miejscu gdzie mogą pojawiü siĊ in-strukcje. Klauzule requires i ensures są specjalnymi przypadkami klauzuli assert.
W adnotacji funkcji klauzula ensures moĪe wykorzystaü specjalną wartoĞü \result dla
oznaczenia wartoĞci zwróconej przez funkcjĊ (zgodnoĞü z JML), alternatywnie nazwĊ wery-fikowanej funkcji (zgodnoĞü z jĊzykiem ST).
Tab. 2. Adaptacja klauzul JML dla jĊzyka ST
Typ Standard JML Adaptacja w ST Zakres
Asercje
assert assert instrukcji
ensures ensures: lokalny
requires requires: lokalny
Modyfikatory lokalizacji
\at \at lub at instrukcji
\old \old instrukcji
Kwantyfikatory \exists \exists mieszany
\forall \forall mieszany
Niezmiennik invariant invariant: instrukcji
Deklaracje
label label: instrukcji
logic logic: globalny
ghost ghost: lokalny
predicate predicate: globalny
axiom axiom: globalny
WartoĞü
zwracana funkcji \result
\result lub
nazwa_funkcji lokalny
Operacje set set: instrukcji
assigns assigns: lokalny
PoprawnoĞü
iteracji variant variant: instrukcji
Weryfikacja jednostki oparta jest na stanach pamiĊci zawierających wartoĞci zmiennych w okreĞlonych momentach wykonywania jednostki [2]. Klauzula \old(zm) reprezentuje
war-toĞü zmiennej o nazwie zm w chwili rozpoczĊcia jednostki. Dla programów i bloków
funkcjo-nalnych jest to równieĪ wartoĞü zmiennej otrzymana na zakoĔczenie poprzedniego cyklu.
2
Stany wykonywania jednostki moĪna nazywaü za pomocą klauzuli label. DostĊp do wartoĞci
zmiennej z zadeklarowanego stanu uzyskuje siĊ za pomocą klauzuli \at(zm,etyk), gdzie etyk jest wczeĞniej zadeklarowaną etykietą stanu. Klauzula assigns wskazuje które zmienne
globalne mogą ulec zmianie podczas wykonywania kodu jednostki.
W zapisie adnotacji mogą pomóc funkcje abstrakcyjne deklarowane za pomocą klauzuli lo-gic, czĊsto wykonywane operacje na zmiennych uĪywanych w asercjach mogą zostaü
zgru-powane w formie funkcji – predykatu poprzez wykorzystanie klauzuli predicate. Aksjomaty
pomocnicze deklaruje siĊ poprzez klauzulĊ axiom. Dodatkowe zmienne lokalne deklarowane
w celu uproszczenia obliczeĔ w wyraĪeniach asercji, nie wystĊpujące w kodzie jednostki, deklaruje siĊ za pomocą klauzuli ghost, a pomocnicze operacje na tych zmiennych moĪna
definiowaü w klauzuli set. Adnotacje do pĊtli w postaci niezmiennika umieszcza siĊ
w klauzuli invariant, a wyraĪenie okreĞlające skoĔczonoĞü pĊtli w klauzuli variant.
Adno-tacje te mogą wykorzystywaü dwa kwantyfikatory – ogólny umieszczany w klauzuli \forall
i szczegóáowy umieszczany w \exists.
Tab. 3. Rozszerzenie JML dla jĊzyka ST
Typ Zapis w ST Zakres
Stany bezpieczne safe_behaviour lokalny
Obsáuga wyjątków general_failure: lokalny requires_failure: lokalny ensures_failure: lokalny Punkty wznowienia resume_after mieszany resume_after_unit mieszany resume_from_unit mieszany resume_from_program mieszany
Punkt zatrzymania terminate_execution mieszany
Jak juĪ wspomniano, standard JML zostaá przewidziany do formalnego zapisu specyfikacji w jĊzyku Java, i nie zdefiniowano w nim elementów typowych dla systemów sterowania. PropozycjĊ rozszerzenia o nowe elementy dla jĊzyka ST przedstawiono w tab. 3. Pierwszym rozszerzeniem jest definicja stanu bezpiecznego. Stan bezpieczny to taki, w którym nie wy-stĊpuje zagroĪenie, spowodowane awarią komponentów systemu sterującego. Definicja ta-kiego stanu dla kaĪdego POU wykorzystuje klauzulĊ safe_behaviour. PoniewaĪ stany
bez-pieczne mogą byü róĪne w zaleĪnoĞci od fazy procesu, dlatego proponuje siĊ aby kaĪdy stan bezpieczny miaá nadaną nazwĊ. Definicja stanu bezpiecznego zawiera kod, który przeáączy wartoĞci zmiennych na odpowiednie wartoĞci, a ostatnią instrukcją tej definicji jest jeden z punktów wznowienia albo zatrzymania.
Punkty wznowienia okreĞlają miejsca od których przetwarzanie zadania sterownika bĊdzie kontynuowane. Punkt resume_after okreĞla wznowienie pracy w miejscu bezpoĞrednio po
sprawdzeniu wyraĪenia asercji. Oznaczenie resume_after_unit wznowi pracĊ w miejscu
nastĊpującym po zakoĔczeniu przetwarzania tego POU, natomiast resume_from_unit
wznowi pracĊ sterownika od początku bieĪącego POU. Punkt resume_from_program ponowi
pracĊ sterownika od początku aktualnie wykonywanego programu. W przeciwieĔstwie do punktów wznowienia punkt zatrzymania (terminate_execution) przerywa pracĊ sterownika
po ustaleniu wartoĞci wyjĞü. W tej sytuacji wznowienie pracy nastąpi dopiero po rĊcznym zresetowaniu sterownika.
Przechwytywanie niespeánionych standardowych asercji requires i ensures powierzono
klauzulom requires_failure i ensures_failure, w których okreĞla siĊ nazwy stanów
bezpiecznych. Podobnie general_failure zawiera stan bezpieczny dla klauzul assert,
któ-rym nie okreĞlono indywidualnego stanu bezpiecznego (assert z jednym argumentem).
Roz-szerzenie to stanowi dozór nad wykonywanym programem, którego realizacjĊ opisano w na-stĊpnym punkcie.
4. REALIZACJA WERYFIKACJI DYNAMICZNEJ
Zadaniem weryfikacji dynamicznej jest sprawowanie dozoru nad wykonywaniem programu. Polega to na sprawdzaniu speánienia warunków początkowych, asercji i warunków koĔco-wych jednostek. W praktyce realizowane jest to przez odpowiednie przeksztaácenia adnotacji do postaci instrukcji operujących na aktualnie wykonywanym kodzie jednostki.
Klauzula (*@ghost: zm : typ; *) przeksztaácana jest podczas kompilacji do postaci VAR zm : typ; END_VAR. Klauzula (*@label: etyk;*) wywoáuje wewnĊtrzną funkcjĊ store-atvars(etyk), której zadaniem jest wykonanie kopii wartoĞci zmiennych z modyfikatorem \at wystĊpujących w adnotacjach. WartoĞci tych zmiennych zostaną oznaczone nazwą
ety-kiety etyk przekazanej w klauzuli label. Klauzula (*@set: ghost_var := expr;*)
zosta-nie przetáumaczona do postaci ghost_var := expr.
a) b)
c)
Rys. 1. Sieci dziaáaĔ weryfikacji dynamicznej dla klauzul: a) requires, b) ensures, c) assert. Asercje táumaczone są do postaci sieci dziaáaĔ. Sieü dla klauzuli requires zostaáa
przedsta-wiona na rys. 1a. Zapis klauzuli táumaczony jest do postaci wyraĪenia warunkowego, którego niespeánienie wywoáuje obsáugĊ stanu bezpiecznego skojarzonego w klauzuli requ-ires_failure. W przypadku, gdy stan bezpieczny zakoĔczony jest punktem powrotu resu-me_after, to przetwarzanie programu jest wznawiane w taki sposób jakby wyraĪenie
warun-kowe zostaáo speánione. Ostatnią instrukcją poprawnego zakoĔczenia klauzuli requires jest
wywoáanie wewnĊtrznej metody storeoldvars(), której zadaniem jest zapamiĊtanie obecnej
Sieü dziaáaĔ dla klauzuli ensures przedstawiono na rys. 1b. W przypadku niespeánienia
wy-raĪenia warunkowego tej klauzuli wywoáywana jest obsáuga stanu bezpiecznego skojarzonego w klauzuli ensures_failure. Gdy definicja stanu bezpiecznego koĔczy siĊ punktem
powro-tu resume_after lub resume_after_unit, to przetwarzanie wznawiane jest od punktu
za-koĔczenia aktualnie sprawdzanej jednostki.
Sieü dziaáaĔ dla klauzuli assert przedstawiono na rys. 1c. Klauzula ta ma dwa warianty.
Wa-riant pierwszy (jednoargumentowy), w przypadku niespeánienia wyraĪenia, obsáuguje stan bezpieczny skojarzony z klauzulą general_failure. Wariant drugi (dwuargumentowy)
ob-sáuguje stan bezpieczny, którego identyfikator zostaá przekazany jako drugi argument. W obu wariantach, gdy obsáuga stanu bezpiecznego koĔczy siĊ punktem resume_after, to
wzna-wiana jest praca sterownika w miejscu nastĊpującym po asercji.
Zastosowanie weryfikacji dynamicznej pozwala zwiĊkszyü bezpieczeĔstwo wykonywanego oprogramowania, poprzez ochronĊ przed niezamierzonym lub celowym wprowadzeniem báĊdnych parametrów, czy poprzez wykrycie uszkodzeĔ czujników. Omawiane w nastĊpnym punkcie przykáady wykorzystują asercyjne rozszerzenia i weryfikacjĊ dynamicznej do detek-cji nieprawidáowych wartoĞci wejĞü ukáadów.
5. PRZYKàADY
Przykáad 1 pochodzi z [9]. Termometr kontaktowy (rys. 2a) generuje sygnaáy a, b, c, d, gdy
temperatura przekroczy odpowiednie wartoĞci. Ukáad sterujący powinien tak generowaü sy-gnaáy dla przeáączników w1, w2, w3, (rys. 2b), aby speániü wymagane warunki wáączeĔ w
za-leĪnoĞci od temperatury t, wymienione na rys. 2a. Styki na rys. 2b narysowano w pozycji 0. a) t < ta – G1 i G2 wáączone ta t < tb – tylko G1 wáączony, tb t < tc – tylko G2 wáączony, tc t < td – G1 i G2 poáączone szeregowo, t td – G1 i G2 wyáączone. b)
Rys. 2. Grzaáki sterowane termometrem, a) sygnaáy ukáadu, b) schemat poáączeĔ grzaáek. Przekroczenie kaĪdego progu temperatury jest sygnalizowane stanem 1 odpowiednich czujni-ków (a – d). Po utworzeniu pierwotnej tablicy stanów wejĞü i odpowiadającym im stanów wyjĞü, którą przedstawiono w tab. 4, przystąpiono do otrzymania równaĔ specyfikujących zachowanie programu poprzez minimalizacjĊ za pomocą tablic Karnaugha. Tablice te wraz z otrzymanymi wzorami zastosowanymi w specyfikacji przedstawiono na rys. 3.
Tab 4. Tablica stanów wejĞü i wyjĞü przykáadu 1 WejĞcia WyjĞcia a b c d w1 w2 w3 0 0 0 0 1 1 0 1 0 0 0 1 0 0 1 1 0 0 0 1 0 1 1 1 0 0 1 1 1 1 1 1 0 0 -
Rys. 3. Tablice Karnaguha oraz wzory specyfikacji przykáadu 1
Kompletny program sterowania wraz z asercyjnym rozszerzeniem zostaá umieszczony na li-stingu 1. Specyfikacja skáada siĊ z dwóch czĊĞci – zgodnej ze standardem JML oraz z czĊĞci spoza JML. CzĊĞü zgodna zawiera klauzulĊ requires w której umieszczono dopuszczalne
kombinacje wartoĞci wejĞü, dla których zostaáy okreĞlone wartoĞci wyjĞü. Klauzula ensures
zawiera wzory specyfikujące zapisane w postaci równowaĪnoĞci (<==> w 8 linii listingu),
z wyjątkiem wyjĞcia w3, które nie zostaáo okreĞlone dla temperatury t td (w tab. 4 i na rys. 3
oznaczone szarym táem). Dla tego przypadku zastosowano w klauzuli ensures implikacjĊ
(==> w 9 linii listingu). CzĊĞü spoza standardu JML zawiera deklaracjĊ stanu bezpiecznego stan_bezp (l. 10-11), którego zadaniem jest przeáączenie wyjĞü w1, w2, w3 w stan 0
logiczne-go. Punkt wznowienia pracy (l. 12) ustalony zostaá w punkcie koĔca kodu jednostki. Niespeá-nienie warunków początkowych lub koĔcowych (l. 12-13) wywoáa obsáugĊ stanu bezpieczne-go stan_bezp.
Listing. 1. Kod programu sterującego grzaákami
01Ň PROGRAM termometr; VAR_EXTERNAL (*$AUTO*) END_VAR;
02Ň (*@REQUIRES: (a = FALSE & b = FALSE & c = FALSE & d = FALSE) OR 03Ň (a = TRUE & b = FALSE & c = FALSE & d = FALSE) OR 04Ň (a = TRUE & b = TRUE & c = FALSE & d = FALSE) OR 05Ň (a = TRUE & b = TRUE & c = TRUE & d = FALSE) OR 06Ň (a = TRUE & b = TRUE & c = TRUE & d = TRUE);
07Ň ASSIGNS: w1, w2, w3;
08Ň ENSURES: (w1 <==> NOT b) & (w2 <==> (NOT a OR (b & NOT d))) & 09Ň (w3 ==> c);
10Ň SAFE_BEHAVIOUR stan_bezp: w1 := FALSE; w2 := FALSE; w3 := FALSE;
11Ň resume_after_unit;
12Ň REQUIRES_FAILURE: stan_bezp;
13Ň ENSURES_FAILURE: stan_bezp; *)
14Ň
15Ň IF NOT a THEN w1 := TRUE; w2 := TRUE; w3 := FALSE;
16Ň ELSIF NOT b THEN w1 := TRUE; w2 := FALSE; w3 := FALSE;
17Ň ELSIF NOT c THEN w1 := FALSE; w2 := TRUE; w3 := FALSE;
18Ň ELSIF NOT d THEN w1 := FALSE; w2 := TRUE; w3 := TRUE; 19Ň ELSE w1 := FALSE; w2 := FALSE; w3 := FALSE;
20Ň END_IF
21Ň
22Ň END_PROGRAM
Tak adnotowany przykáad skompilowany do weryfikacji dynamicznej, zapewnia elementarną ochronĊ przed niedozwolonymi wartoĞciami czujników w trakcie wykonania, a takĪe automa-tycznie przeáączy wyjĞcia do stanu bezpiecznego w przypadku wykrycia niespójnoĞci pomiĊ-dzy specyfikacją ukáadu sterowana, a jego realizacją. JednoczeĞnie zostaáa zachowana przej-rzystoĞü kodu pomiĊdzy czĊĞcią sterującą, a czĊĞcią odpowiedzialną za sprawdzenie popraw-noĞci wejĞü.
Przykáad 2 zaczerpniĊto z [4]. PrzenoĞnik taĞmowy transportuje káody drewna (rys. 4). Na taĞmociągu dokonuje siĊ pomiaru dáugoĞci káody za pomocą czujników B1, B2, B3.
Przysáo-niĊcie jednego z czujników generuje na jego wyjĞciu logiczną jedynkĊ. Káody krótkie, to ta-kie których dáugoĞü jest mniejsza od rozstawu czujników pomiaru dáugoĞci (zakáada siĊ jed-nakowy rozstaw czujników do pomiaru dáugoĞci). ĝrednie mają dáugoĞü od rozstawu czujni-ków do podwojonej tej dáugoĞci. Káody dáugie mają dáugoĞü wiĊkszą niĪ podwojony rozstaw czujników. Zadaniem ukáadu do sortowania drewna jest skierowanie káód krótkich do komory 1, Ğrednich do komory 2, a dáugich przetransportowanie do koĔca taĞmociągu w celu dalszej obróbki. Do kierowania káodami wykorzystuje siĊ wypychacze, sterowane wyjĞciami Q1 i Q2.
PozycjĊ káody na taĞmie wskazują czujniki B7 i B8, a opuszczenie przez káodĊ taĞmy czujniki B4, B5 i B6. Wprowadzenie nastĊpnej káody na taĞmociąg moĪliwe jest tylko wtedy, gdy
po-przednia opuĞci go. Sygnalizowane jest to za pomocą Ğwiateá Q3 i Q4.
Rys. 4. Ukáad czujników w urządzeniu do sortowania drewna
Automat Moore’a sterujący urządzeniem do sortowania drewna wraz z tablicą wartoĞci wyjĞü stanów przedstawiono na rys. 5. Znaczenie stanów jest nastĊpujące: 0 – taĞmociąg pusty, moĪna wprowadziü káodĊ; 1 – początek pomiaru dáugoĞci káody; 2 – káoda krótka, oczekiwa-nie na dojazd káody do wypychacza 1; 3 – wypychanie káody krótkiej; 4 – oczekiwanie na opuszczenie taĞmociągu przez krótką káodĊ; 5 – pomiar dáugoĞci káody; 6 – káoda dáuga, oczekiwanie na dojazd káody do koĔca taĞmociągu; 7 – oczekiwanie na opuszczenie taĞmo-ciągu przez káodĊ; 8 – káoda Ğrednia, oczekiwanie na dojazd do wypychacza 2; 9 – wypycha-nie káody Ğredwypycha-niej; 10 – oczekiwanie na opuszczenie taĞmociągu przez káodĊ Ğrednią.
Automat zaimplementowano w jĊzyku ST jako dwie instrukcje wyboru (case), przedstawione na listingu 2. Pierwsza z nich (linia 25) odpowiada za przejĞcia pomiĊdzy stanami, a druga (l. 43) za ustawienie wartoĞci wyjĞü otrzymanego stanu. Do programu dodano równieĪ adnotacje specyfikacji w postaci warunków wstĊpnych (l. 3), modyfikowanych zmiennych globalnych (l. 4), warunków koĔcowych (l. 5 – 17) i dwóch stanów bezpiecznych (l. 18 – 21). Niespeá-nienie warunku początkowego lub koĔcowego skojarzono ze stanem bezpiecznym sys-tem_blad, którego obsáuga przeáącza wszystkie wyjĞcia w stan 0 i powoduje zatrzymanie
pracy sterownika. Warunek koĔcowy powstaá na podstawie automatu i zawiera implikacje poáączone koniunkcją. KaĪda z implikacji odpowiada jednemu przejĞciu pomiĊdzy stanami. Poprzednik implikacji skáada siĊ z wartoĞci zmiennej stan z modyfikatorem \old
wskazują-cym stan automatu w poprzednim cyklu, oraz warunku przejĞcia. NastĊpnik implikacji skáada siĊ z nowego stanu automatu oraz wymaganym stanem wyjĞü. Wykrywanie niesprawnoĞci czujników odbywa siĊ poprzez osobne asercje oznaczone w listingu szarym táem. W przypadku wykrycia báĊdnych wskazaĔ czujników zostanie wywoáana obsáuga stanu bez-piecznego czujnik_blad, którego zadaniem jest wyáączenie wypychaczy i zaĞwiecenie obu
lamp sygnalizujących niezdatnoĞü pracy ukáadu.
Listing. 2. Kod programu realizujący ukáad sterowania sortownicą
01Ň PROGRAM sortownica; VAR_EXTERNAL (*$AUTO*) END_VAR;
02Ň VAR stan:INT; END_VAR
03Ň (*@REQUIRES: stan>=0 & stan<=10;
04Ň ASSIGNS: Q1, Q2, Q3, Q4;
05Ň ENSURES: (\old(stan)=0 & B1 ==> stan=1 & Q1=0 & Q2=0 & Q3=1 & Q4=0) 06Ň & (\old(stan)=1 & NOT B1 & B2 ==> stan=2 & Q1=0 & Q2=0 & Q3=1 & Q4=0) 07Ň & (\old(stan)=1 & B1 & B2 ==> stan=5 & Q1=0 & Q2=0 & Q3=1 & Q4=0) 08Ň & (\old(stan)=2 & B7 ==> stan=3 & Q1=1 & Q2=0 & Q3=1 & Q4=0) 09Ň & (\old(stan)=3 & B4 ==> stan=4 & Q1=1 & Q2=0 & Q3=1 & Q4=0) 10Ň & (\old(stan)=4 & NOT B4 ==> stan=0 & Q1=0 & Q2=0 & Q3=0 & Q4=1)
11Ň & (\old(stan)=5 & B1 & B2 & B3 ==> stan=6 & Q1=0 & Q2=0 & Q3=1 & Q4=0) 12Ň & (\old(stan)=5 & NOT B1 & B2 & B3 ==> stan=8 & Q1=0 &Q2=0 & Q3=1 & Q4=0)
13Ň & (\old(stan)=6 & B6 ==> stan=7 & Q1=0 & Q2=0 & Q3=1 & Q4=0) 14Ň & (\old(stan)=7 & NOT B6 ==> stan=0 & Q1=0 & Q2=0 & Q3=0 & Q4=1) 15Ň & (\old(stan)=8 & B8 ==> stan=9 & Q1=0 & Q2=1 & Q3=1 & Q4=0) 16Ň & (\old(stan)=9 & B5 ==> stan=10 & Q1=0 & Q2=1 & Q3=1 & Q4=0) 17Ň & (\old(stan)=10 & NOT B5 ==> stan=0 & Q1=0 & Q2=0 & Q3=0 & Q4=1);
18Ň SAFE_BEHAVIOUR czujnik_blad: Q1:=0; Q2:=0; Q3:=1; Q4:=1; 19Ň resume_after_unit; 20Ň SAFE_BEHAVIOUR system_blad: Q1:=0; Q2:=0; Q3:=0; Q4:=0; 21Ň terminate_execution; 22Ň REQUIRES_FAILURE: system_blad; 23Ň ENSURES_FAILURE: system_blad; *) 24Ň 25Ň CASE stan OF
26Ň 0: IF B1 THEN stan:=1; END_IF
27Ň 1: (*@ASSERT(NOT (B1 AND NOT B2 AND B3), czujnik_blad); *)
28Ň IF B1 & B2 THEN stan:=5; ELSIF NOT B1 & B2 THEN stan:=2; END_IF
29Ň 2: (*@ASSERT(NOT (B8 OR B6 OR B5), czujnik_blad); *) 30Ň IF B7 THEN stan:=3; END_IF
31Ň 3: IF B4 THEN stan:=4; END_IF 32Ň 4: IF NOT B4 THEN stan:=0; END_IF
33Ň 5: (*@ASSERT(NOT (B1 AND NOT B2 AND B3), czujnik_blad); *)
34Ň IF B1&B2 &B3 THEN stan:=6; ELSIF NOTB1 &B2 & B3THEN stan:=8; END_IF
35Ň 6: (*@ASSERT(NOT (B7 OR B8 OR B5 OR B4), czujnik_blad); *) 36Ň IF B6 THEN stan:=8; END_IF
38Ň 8: (*@ASSERT(NOT (B7 OR B6 OR B4), czujnik_blad); *) 39Ň IF B8 THEN stan:=9; END_IF
40Ň 9: IF B5 THEN stan:=10; END_IF
41Ň 10: IF NOT B5 THEN stan:=0; END_IF
42Ň END_CASE 43Ň CASE stan OF 44Ň 0: Q1:=0; Q2:=0; Q3:=0; Q4:=1; 45Ň 1..2,5..8: Q1:=0; Q2:=0; Q3:=1; Q4:=0; 46Ň 3,4: Q1:=1; Q2:=0; Q3:=1; Q4:=0; 47Ň 9,10: Q1:=0; Q2:=1; Q3:=1; Q4:=0; 48Ň END_CASE END_PROGRAM
W drugim przykáadzie sprawdzenie poprawnoĞci wyjĞü czujników odbywa siĊ w tych sta-nach, w których moĪliwe jest wykrycie báĊdów. Przeksztaácenie wykorzystanych asercji do pojedynczej klauzuli requires znacznie skomplikowaáoby jej zapis, co uczyniáoby ją trudną
do odczytania przez inne osoby.
6. PODSUMOWANIE
Przedstawiono asercyjne rozszerzenie jĊzyka ST do projektowania kontraktowego oraz wery-fikacji dynamicznej systemów sterowania. Cechą charakterystyczną prezentowanego rozsze-rzenia jest podobieĔstwo do innych jĊzyków BISL, wykorzystywanych we wspóáczesnym projektowaniu oprogramowania. Uzupeániając popularne klauzule standardu JML o deklaracje stanów bezpiecznych i punktów wznowienia, moĪna przeprowadziü weryfikacjĊ dynamiczną opracowanego rozwiązania. Sprawdzanie asercji podczas wykonywania progra-mu zwiĊksza bezpieczeĔstwo wykonywanego prograprogra-mu poprzez diagnostykĊ wejĞü ukáadu i chroni przed niezamierzonym lub celowym wprowadzeniem báĊdnych parametrów. Zapis wykorzystujący adnotacje oddziela wáaĞciwy kod systemu sterowania od jego diagnostyki, co czyni go przejrzystym i lĪejszym do analizy przez inne osoby.
Dalsze prace bĊdą dotyczyáy opracowania kompilatora do transformacji kodu jĊzyka ST z adnotacjami do ANSI C, oraz implementacji asercyjnego rozszerzenia do weryfikacji dy-namicznej w pakiecie CPDev.
BIBLIOGRAFIA
1. Baudin P., Cuoq P., Filliâtre J.Ch., Marché C., Monate B., Moy Y., Prevosto V.: ACSL: ANSI/ISO C Specification Language. http://frama-c.cea.fr.
2. Bornat R.: Proving pointer programs in Hoare logic. Mathematics of Program Construc-tion. MPC '00 Proceedings, pp. 102–126. Springer-Verlag, London, 2000.
3. Filliâtre J.Ch. The WHY verification tool. Tutorial and Reference Manual. http://www.lri.fr.
4. Kasprzyk J., Jegierski T., Wyrwaá J., Hajda J.: Programowanie sterowników PLC. Wy-dawnictwo Pracowni Komputerowej Jacka Skalmierskiego, Gliwice, 1998.
5. Leavens G.: An Overview of Larch/C++: Behavioral Specifications for C++ Modules. [w:] Kilov H., Harvey W. (red): Specification of Behavioral Semantics in Object-Oriented Information Modeling. Kluwer Academic Publishers, 1996.
6. Leavens G., Baker A., Ruby C.: JML: a Notation for Detailed Design. [w:] Kilov H., Rumpe B., Simmonds I. (red): Behavioral Specifications of Businesses and Systems, 99. 7. Meyer B.: Applying “design by contract”. Computer, 25(10), pp. 40–51, 1992.
8. Meyer B.: Eiffel: The Language. Object-Oriented Series. Prentice Hall New York, 1992. 9. ĝwider Z. (red.): Sterowniki mikroprocesorowe. Oficyna Wydawnicza Politechniki
