II. OVERVIEW OF THE REUSABLE AUTOMATION COMPONENTОсновні частини RAC для побудови програм управління ПЛК наведені ліворуч. Праворуч показана структура специфікації для ПЛК-орієнтованих моделей див розділ III.
Надалі слово "компонент" використовується тільки в контексті РАК. Рак має інтерйес і тіло. Інтерфейс складається з входів(I), виходів(O) і специфікації. Тіло реалізує функції компоненту і декларує будь які внутрішні змінні (V). Тіло доступне тільки для розробників компоненту (інкапсуляція). Специфікація РАК розроблена для використання формальної верифікації, для перевірки чи відповідає реалізація повністю специфікації.
Основні принципи побудови РАК носять загальний характер і відкриті для різних мов програмування для реалізації. Приклади реалізацій є на ФБ для IEC 61131-3 та IEC 61499. У реалізації RAC оновлення може бути як на основі циклу (IEC 61131-3) так на основі подій (IEC 61499). Коли RAC оновлюється нові значення виходів і внутрішніх змінних обчислюються в залежності від поточних значень вхідних і внутрішніх значень змінних.
Таким чином, кожне оновлення позначається унікальним індексом
K є N, воно збільшується на одиницю з кожним апдейтом блоку.
Формальне визначення RAC, I,O,V,f дані в секції V.
Хоча неформальні описи в RAC (природною мовою, картинки і т.д.) може допомогти в розумінні RAC, такі описи не підходять для формальної верифікації, так як вони можуть бути неоднозначними і можуть бути неправильно витлумачені. Формальна верифікація вимагає формальної специфікації. Таким чином, RAC доповнюється формальними специфікаціями. Формальна специфікація може розглядатися як однозначна абстракція реалізації; Наприклад, вона може вказати, що певна комбінація входів завжди призводить до певної комбінації виходів.
Структура специфікації базується на концепції "Дизайну за контрактом" [9]. Проектування за контрактом був введений Бертраном Мейером, щоб отримати надійні і повторно-використовувані об'єктно-орієнтовані програми на мові програмування Eiffel. Для кожної процедури програмного забезпечення, договір може виразити парою передумови і постумови. Передумова висловлює вимоги, яким повинен задовільняти виклик підпрограми, для гарантування постумови.