State Machines as Inductive Types(Concurrent Systems)

スポンサーリンク

概要

• 論文の詳細を見る

• We describe a way to write state machines inductively. The proposed method makes it possible to use the standard techniques for proving theorems on inductive types to verify that state machines satisfy invariant properties. A mutual exclusion protocol using a queue is used to exemplify the proposed method.

• 社団法人電子情報通信学会の論文
• 2007-12-01

著者

• Ogata Kazuhiro

  School Of Information Science Japan Advanced Institute Of Science And Technology (jaist)

• Ogata Kazuhiro

  Jaist Nomi‐shi Jpn

• Ogata Kazuhiro

  School Of Information Science Jaist

• FUTATSUGI Kokichi

  School of Information Science, JAIST

• Futatsugi Kokichi

  School Of Information Science Jaist

関連論文

• State Machines as Inductive Types(Concurrent Systems)
• Proof Score Approach to Verification of Liveness Properties
• Analysis of membership sharing in digital subscription services
• Towards Reliable E-Government Systems with the OTS/CafeOBJ Method
• A Specification Translation from Behavioral Specifications to Rewrite Specifications
• Comparison of Maude and SAL by Conducting Case Studies Model Checking a Distributed Algorithm(Concurrent Systems)
• A Behavioral Specification of Imperative Programming Languages
• Concurrent Reflective Computations in Rewriting Logic(Theory of Rewriting Systems and Its Applications)
• A Scenario-based Object-Oriented Modeling Method with Algebraic
• A Note on "On the Construction of Boolean Functions with Optimal Algebraic Immunity"

スポンサーリンク