Описание формальной модели операционной системы.

Рассмотрим работу блоков ОС в виде формальной модели для абстрактной многопроцессорной ЭВМ. Т=[t₀,t₁] , где t₀ –время инициирования, t₁- время уничтожения системы. Структура ОС в некоторый момент времени tєT может быть представлен графом Г_t , где Р={p₀,p₁…p_n}- класс процессов, R ={r₁, r₂,…,r_q} – класс ресурсов. Элементы множеств являются вершинами графа Г_t . Считаем, что P и R конечные и непустые множества. Т.к. ОС является динамически изменяющейся системой, то в некоторый момент времени t₁, t₂ єT; t₁≠t₂ структура может быть представлена графами Г_t1­, Г_t2. Рассмотрим изменение графа Г_t , отражающего структуру ОС в любой момент времени tєT. Выделим в некоторое множество σвсе возможные вершины и ребра, которые могут быть получены [t₀,t_k]. Каждый элемент множества σ(вершину или ребро) обозначим через σ_jj≥1. Определим множество Екак совокупность правил, фиксирующих изменение структуры графа Г_t для любого tєT. Каждое правило из множества Ебудет иметь вид:

Гденомер правила.

означает , что в момент времени tєT заменяется на набор элементов

означает номер правила, на которое осуществляется переход, если активен или блокирован.

Пусть V – множество номеров правил из Е. σ₀ некоторый начальный процесс, инициирующий работу системы. Тогда М – формальная модель ОС, может быть определена:М=<Т,σ, Е, V, σ₀>