Visual specifications of policies and their verification

被引：0
|
作者：
Koch, M [1 ]
Parisi-Presicce, F
机构：
[1] Free Univ Berlin, D-1000 Berlin, DE, Germany
[2] Univ Roma La Sapienza, Rome, IT, Italy
[3] George Mason Univ, Fairfax, VA 22030 USA
来源：
FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING, PROCEEDINGS | 2003年 / 2621卷
关键词：
D O I：
暂无
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
The specification of policies is a crucial aspect in the development of complex systems, since policies control the system's behavior. In order to predict a possibly incorrect behavior of the system, it is necessary to have a precise specification of the policy, better if described in an intuitive formalism. We propose policy specifications in three modeling notations, viz. UML, Alloy and Graph Transformations, and compare them from the viewpoint of readability, verifiability as well as tool support. We use a role-based access control policy as example policy.
引用
收藏
页码：278 / 293
页数：16
相关论文
共 50 条
  • [31] Formal Verification of AADL Specifications in the Topcased Environment
    Berthomieu, Bernard
    Bodeveix, Jean-Paul
    Chaudet, Christelle
    Dal Zilio, Silvano
    Filali, Mamoun
    Vernadat, Francois
    RELIABLE SOFTWARE TECHNOLOGIES - ADA-EUROPE 2009, 2009, 5570 : 207 - +
  • [32] A simulation approach to verification and validation of formal specifications
    Liu, SY
    FIRST INTERNATIONAL SYMPOSIUM ON CYBER WORLDS, PROCEEDINGS, 2002, : 113 - 120
  • [33] Formal Verification of Security Specifications with Common Criteria
    Morimoto, Shoichi
    Shigematsu, Shinjiro
    Goto, Yuichi
    Cheng, Jingde
    APPLIED COMPUTING 2007, VOL 1 AND 2, 2007, : 1506 - +
  • [34] SPECIFICATIONS - THE REAL DESIGN-VERIFICATION PROBLEM
    KAUFMAN, PA
    COMPUTER DESIGN, 1989, 28 (11): : 73 - 73
  • [35] Inductive Temporal Formula Specifications for System Verification
    Yamada, Chikatoshi
    Nagata, Yasunori
    Nakao, Zensho
    JOURNAL OF ADVANCED COMPUTATIONAL INTELLIGENCE AND INTELLIGENT INFORMATICS, 2005, 9 (03) : 321 - 328
  • [36] Rich Specifications for Ethereum Smart Contract Verification
    Braem, Christian
    Eilers, Marco
    Mueller, Peter
    Sierra, Robin
    Summers, Alexander J.
    PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2021, 5 (OOPSLA):
  • [37] Automatic Verification of Parametric Specifications with Complex Topologies
    Faber, Johannes
    Ihlemann, Carsten
    Jacobs, Swen
    Sofronie-Stokkermans, Viorica
    INTEGRATED FORMAL METHODS, 2010, 6396 : 152 - +
  • [38] Expressive program verification via structured specifications
    Gherghina, Cristian
    David, Cristina
    Qin, Shengchao
    Chin, Wei-Ngan
    INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER, 2014, 16 (04) : 363 - 380
  • [39] Quantum Circuits Specifications Design with Lexical Verification
    Kalmychkov, V. A.
    Krasilnikov, A. V.
    Matveeva, I. V.
    2015 XVIII International Conference on Soft Computing and Measurements (SCM), 2015, : 87 - 89
  • [40] Verification of Unit and Dimensional Consistencies in Polychronous Specifications
    Nanjundappa, Mahesh
    Shukla, Sandeep K.
    PROCEEDINGS OF THE 2014 FORUM ON SPECIFICATION & DESIGN LANGUAGES (FDL), 2014,
12345