APPARATUS AND METHOD FOR PERFORMING FORMAL VERIFICATION OF HIERARCHICAL REAL-TIME SCHEDULING SYSTEM

摘要

Disclosed are a formal verification method comprising a formal specification generating unit and a formal verification performing unit, and a formal verification apparatus using the same, in a real-time system in which a scheduler exists in a hierarchical manner. The formal verification apparatus comprises: an input unit for receiving inputted requirements of the system; a formal specification generating unit for receiving the requirements and generating formal specifications by using a timed automata-based formalization technique; and a formal verification performing unit for performing verification on the formal specifications by using a model checking tool. The formal specification generating unit includes: a top scheduler model generating unit for specifying a model of a top scheduler of the system; a sub-scheduler model generating unit for specifying at least one sub-scheduler model of the system; and a task model generating unit for specifying at least one task.;COPYRIGHT KIPO 2017