シーケンス制御系の設計と検証
藤野 和久 (9751093)
一方，近年のPC(Programmable Controller)の普及にともない，PCに対する新しいプログラミングテクニックとしてSFC(Sequential Function Chart)によるプログラミングが提案されている．SFCはラダー図とは異なり，動作シーケンスが陽に表される，プログラムを構造化できるといった特徴があるものの，プログラムの検証のためには付属プロセスの挙動をモデル化する必要がある．
本研究では，SFCからペトリネットへの変換則を導出し，SFCをモデル化する．また，制御対象も離散事象システムとしてペトリネットを用いてモデル化する．そして，ペトリネットシミュレータを用いてのシミュレーションを行う方法を推奨する．
また，SFCプログラムの検証のため，ペトリネットを用いてモデル化したシーケンス制御系が，時相論理式で表された仕様を満たすかどうかをモデルチェッキングを用いて検証する方法も提案する．