Towards Reliable E-Government Systems with the OTS/CafeOBJ Method
スポンサーリンク
概要
- 論文の詳細を見る
System implementation for e-Government initiatives should be reliable. Unreliable system implementation could, on the one hand, be insufficient to fulfill basic system requirements, and more seriously on the other hand, break the trust of citizens on governments. The objective of this paper is to advocate the use of formal methods in general, the OTS/CafeOBJ method in particular in this paper, to help develop reliable system implementation for e-Government initiatives. An experiment with the OTS/CafeOBJ method on an e-Government messaging framework proposed for providing citizens with seamless public services is described to back up our advocation. Two previously not well-clarified problems of the framework and their potential harm realized in this experiment are reported, and possible ways of revisions to the framework are suggested as well. The revisions are proved to be sufficient for making the framework satisfy certain desired properties.
- (社)電子情報通信学会の論文
- 2010-05-01
著者
-
Ogata Kazuhiro
School Of Information Science Japan Advanced Institute Of Science And Technology (jaist)
-
Ogata Kazuhiro
School Of Information Science Jaist
-
FUTATSUGI Kokichi
School of Information Science, JAIST
-
KONG Weiqiang
School of Information Science, Japan Advanced Institute of Science and Technology (JAIST)
-
Kong Weiqiang
School Of Information Science Japan Advanced Institute Of Science And Technology (jaist)
-
Futatsugi Kokichi
School Of Information Science Jaist
-
Ogata Kazuhiro
School of Information Science, Japan Advanced Institute of Science and Technology (JAIST)
-
FUTATSUGI Kokichi
School of Information Science
関連論文
- User-defined on-demand matching
- 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
- Algebraic approaches to formal analysis of the mondex electronic purse system
- 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"
- A Note on "On the Construction of Boolean Functions with Optimal Algebraic Immunity"
- From Fault Tree Analysis to Formal System Specification and Verification with OTS/CafeOBJ