Formalization and analysis of public administration domain with the OTS/CafeOBJ method

Xiaoyi Chen, Jianwen Xiang, Weiqiang Kong, Kokichi Futatsugi

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Government transparency should be embedded in the designs of e-Government systems. Lack of transparency can prevent the public from participating actively in government operation, such as by raising questions and protesting ill-advised decisions, which in turn may lead to concealment official graft or favouritism. However, it is also difficult to guarantee that designs of e-Government systems are consistent with real requirements in terms of having desired properties, such as transparency. In this paper, we introduce formal methods into the field of e-Government (or public administration) for formalizing designs of e-Government systems and analyzing if the designs satisfy desired properties, in particular transparency. To the best of our knowledge, we are the first to try to formally define and analyze the notion of transparency based on the formalized designs of e-Government systems. The formal method that we used is an equation-based method - the OTS/CafeOBJ method. In using this method, an e-Government system design is first modeled as an Observational Transition System (OTS), a kind of transition system that can be straightforwardly written in terms of equations. The OTS is then specified in CafeOBJ, an algebraic specification language. And lastly, we express the transparency properties as invariants of the OTS, and verify the invariants by using the CafeOBJ system as an interactive theorem prover.

Original languageEnglish
Title of host publicationICEG 2007 - 3rd International Conference on e-Government
PublisherAcademic Conferences Limited
Pages77-86
Number of pages10
ISBN (Print)9781905305582
Publication statusPublished - Jan 1 2007
Event3rd International Conference on e-Government, ICEG 2007 - Montreal, QC, Canada
Duration: Sep 27 2007Sep 28 2007

Publication series

NameICEG 2007 - 3rd International Conference on e-Government

Other

Other3rd International Conference on e-Government, ICEG 2007
CountryCanada
CityMontreal, QC
Period9/27/079/28/07

Fingerprint

Public administration
formalization
public administration
Transparency
electronic government
transparency
Formal methods
Specification languages
Grafts
Systems analysis
guarantee

All Science Journal Classification (ASJC) codes

  • Computer Networks and Communications
  • Law

Cite this

Chen, X., Xiang, J., Kong, W., & Futatsugi, K. (2007). Formalization and analysis of public administration domain with the OTS/CafeOBJ method. In ICEG 2007 - 3rd International Conference on e-Government (pp. 77-86). (ICEG 2007 - 3rd International Conference on e-Government). Academic Conferences Limited.

Formalization and analysis of public administration domain with the OTS/CafeOBJ method. / Chen, Xiaoyi; Xiang, Jianwen; Kong, Weiqiang; Futatsugi, Kokichi.

ICEG 2007 - 3rd International Conference on e-Government. Academic Conferences Limited, 2007. p. 77-86 (ICEG 2007 - 3rd International Conference on e-Government).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Chen, X, Xiang, J, Kong, W & Futatsugi, K 2007, Formalization and analysis of public administration domain with the OTS/CafeOBJ method. in ICEG 2007 - 3rd International Conference on e-Government. ICEG 2007 - 3rd International Conference on e-Government, Academic Conferences Limited, pp. 77-86, 3rd International Conference on e-Government, ICEG 2007, Montreal, QC, Canada, 9/27/07.
Chen X, Xiang J, Kong W, Futatsugi K. Formalization and analysis of public administration domain with the OTS/CafeOBJ method. In ICEG 2007 - 3rd International Conference on e-Government. Academic Conferences Limited. 2007. p. 77-86. (ICEG 2007 - 3rd International Conference on e-Government).
Chen, Xiaoyi ; Xiang, Jianwen ; Kong, Weiqiang ; Futatsugi, Kokichi. / Formalization and analysis of public administration domain with the OTS/CafeOBJ method. ICEG 2007 - 3rd International Conference on e-Government. Academic Conferences Limited, 2007. pp. 77-86 (ICEG 2007 - 3rd International Conference on e-Government).
@inproceedings{8b228e4bb1ed4a8e809c53492af34bd6,
title = "Formalization and analysis of public administration domain with the OTS/CafeOBJ method",
abstract = "Government transparency should be embedded in the designs of e-Government systems. Lack of transparency can prevent the public from participating actively in government operation, such as by raising questions and protesting ill-advised decisions, which in turn may lead to concealment official graft or favouritism. However, it is also difficult to guarantee that designs of e-Government systems are consistent with real requirements in terms of having desired properties, such as transparency. In this paper, we introduce formal methods into the field of e-Government (or public administration) for formalizing designs of e-Government systems and analyzing if the designs satisfy desired properties, in particular transparency. To the best of our knowledge, we are the first to try to formally define and analyze the notion of transparency based on the formalized designs of e-Government systems. The formal method that we used is an equation-based method - the OTS/CafeOBJ method. In using this method, an e-Government system design is first modeled as an Observational Transition System (OTS), a kind of transition system that can be straightforwardly written in terms of equations. The OTS is then specified in CafeOBJ, an algebraic specification language. And lastly, we express the transparency properties as invariants of the OTS, and verify the invariants by using the CafeOBJ system as an interactive theorem prover.",
author = "Xiaoyi Chen and Jianwen Xiang and Weiqiang Kong and Kokichi Futatsugi",
year = "2007",
month = "1",
day = "1",
language = "English",
isbn = "9781905305582",
series = "ICEG 2007 - 3rd International Conference on e-Government",
publisher = "Academic Conferences Limited",
pages = "77--86",
booktitle = "ICEG 2007 - 3rd International Conference on e-Government",

}

TY - GEN

T1 - Formalization and analysis of public administration domain with the OTS/CafeOBJ method

AU - Chen, Xiaoyi

AU - Xiang, Jianwen

AU - Kong, Weiqiang

AU - Futatsugi, Kokichi

PY - 2007/1/1

Y1 - 2007/1/1

N2 - Government transparency should be embedded in the designs of e-Government systems. Lack of transparency can prevent the public from participating actively in government operation, such as by raising questions and protesting ill-advised decisions, which in turn may lead to concealment official graft or favouritism. However, it is also difficult to guarantee that designs of e-Government systems are consistent with real requirements in terms of having desired properties, such as transparency. In this paper, we introduce formal methods into the field of e-Government (or public administration) for formalizing designs of e-Government systems and analyzing if the designs satisfy desired properties, in particular transparency. To the best of our knowledge, we are the first to try to formally define and analyze the notion of transparency based on the formalized designs of e-Government systems. The formal method that we used is an equation-based method - the OTS/CafeOBJ method. In using this method, an e-Government system design is first modeled as an Observational Transition System (OTS), a kind of transition system that can be straightforwardly written in terms of equations. The OTS is then specified in CafeOBJ, an algebraic specification language. And lastly, we express the transparency properties as invariants of the OTS, and verify the invariants by using the CafeOBJ system as an interactive theorem prover.

AB - Government transparency should be embedded in the designs of e-Government systems. Lack of transparency can prevent the public from participating actively in government operation, such as by raising questions and protesting ill-advised decisions, which in turn may lead to concealment official graft or favouritism. However, it is also difficult to guarantee that designs of e-Government systems are consistent with real requirements in terms of having desired properties, such as transparency. In this paper, we introduce formal methods into the field of e-Government (or public administration) for formalizing designs of e-Government systems and analyzing if the designs satisfy desired properties, in particular transparency. To the best of our knowledge, we are the first to try to formally define and analyze the notion of transparency based on the formalized designs of e-Government systems. The formal method that we used is an equation-based method - the OTS/CafeOBJ method. In using this method, an e-Government system design is first modeled as an Observational Transition System (OTS), a kind of transition system that can be straightforwardly written in terms of equations. The OTS is then specified in CafeOBJ, an algebraic specification language. And lastly, we express the transparency properties as invariants of the OTS, and verify the invariants by using the CafeOBJ system as an interactive theorem prover.

UR - http://www.scopus.com/inward/record.url?scp=84902465628&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84902465628&partnerID=8YFLogxK

M3 - Conference contribution

AN - SCOPUS:84902465628

SN - 9781905305582

T3 - ICEG 2007 - 3rd International Conference on e-Government

SP - 77

EP - 86

BT - ICEG 2007 - 3rd International Conference on e-Government

PB - Academic Conferences Limited

ER -