RTOSライブラリ - Toshiaki Aoki's Home PageμITRON RTOS用ライブラリ for PROmela/spiN (μIPRON) μIPRONは，「μITRON RTOS用ライブラリ for PROmela/spiN」の省略名です． 「マイクロアイプロン」と発音してください μIPRONはモデル検査ツールspinを用いて，μITRON仕様のRTOS(Real-Time Operating System)上で動作するマルチタスクソフトウェアを検証するためのライ ブラリです．Spinの入力言語では，μITRONなどのRTOSで使う優先度や sleep/wakeupなどの概念を直接的に記述することができません．そこで，これらの 概念が取り扱えるようなライブラリμIPRONを作りました．μIPRONでは，μITRON の挙動をpromela/spinでエミュレーションします．これにより，promelaでμITRON
