Metody formalnej analizy systemów wbudowanych czasu rzeczywistego
W niniejszej rozprawie zastosowano nowatorski język modelowania formalnego Alvis. Język ten został opracowany i jest nadal rozwijany w Katedrze Informatyki Stosowanej na Wydziale Elektrotechniki, Automatyki, Informatyki i Inżynierii Biomedycznej Akademii Górniczo-Hutniczej w Krakowie. Głównym celem niniejszej rozprawy było opracowanie rozszerzenia języka Alvis na potrzeby modelowania wbudowanych systemów czasu rzeczywistego, z założeniem, że działają one na platformie jednoprocesorowej. W tym celu opracowano nową warstwę systemowa języka Alvis, która przede wszystkim uwzględnia aspekty związane z czasem oraz definiuje algorytm szeregowania zadań systemu czasu rzeczywistego. Na potrzeby stosowania nowej warstwy systemowej opracowano i zaimplementowano nowy algorytm wyznaczania etykietowanych systemów przejść. Implementacja jest rozszerzeniem stosowanej w środowisku Alvis reprezentacji IHR (Intermediate Haskell Representation), przez co stanowi naturalny etap rozwoju języka Alvis i wspierającego go oprogramowania. Niniejsza rozprawa zawiera także studium przypadków, w którym pokazano praktyczne wykorzystanie Alvisa do tworzenia modeli formalnych, dla dwóch systemów czasu rzeczywistego.This dissertation uses the innovative Alvis formal modeling language. This language has been developed and is still being developed at the Department of Applied Computer Science at the Faculty of Electrical Engineering, Automatics, Computer Science and Biomedical Engineering of the AGH University of Science and Technology in Krakow. The main purpose of this dissertation was to develop the Alvis language extension for modeling embedded real-time systems, with the assumption that they operate on a single-processor platform. To this end, a new system layer has been developed, which primarily takes into account the aspects related to time and defines the algorithm for scheduling real time system’s tasks. For the use of a new system layer new algorithm for determining labeled transition systems was developed and implemented. Implementation is an extension of IHR (Intermediate Haskell Representation) used in the Alvis environment, therefore, it constitutes a natural stage in the development of Alvis language and supporting software. This dissertation also includes a case study that shows the practical use of Alvis to create formal models for two real-time systems.
