オートマトンモデルに基づいたディジタルロジックの仕様化と検証  [in Japanese] Specification and Verification of Digital Logic Based on Automaton Model  [in Japanese]

形式手法の応用として,仕様記述言語E.LOTOS,SDLに基づいたディジタルロジックの仕様化に関する研究がこれまでに行われてきている.また,同目的のための応用とは異なるが,リアルタイムシステムの仕様化のための時相論理に基づいたTILCOや,PLC(Programmable Logic Controller)の仕様化のためのPLCオートマトンが提案されてきている.本稿では,以上の研究の背景を踏まえ,ディジタルロジックやPLCの仕様化及び検証を目的とする新たなオートマトンモデルについて考察する.

As application of formal methods, there have been researches for specification of digital logic, based on E-LOTOS and SDL. 0n the other hand, TILCO, based on temporal logic, and PLC-automata have been proposed for real-time system specification and for PLC (Programmable Logic Controller) specification, respectively. In this paper, on the basis of the above researches, we consider a new automaton model for specification and verification of digital logic, PLC and so on.