• Article
  • | |
  • Metrics
  • |
  • Reference [21]
  • |
  • Related [20]
  • |
  • Cited by [1]
  • | |
  • Comments
    Abstract:

    Distributed control systems are a category of high complex systems that include a large number of devices controlled and harmonized by computer systems. Their reliability and functional correctness always need to be guaranteed as their mission-critical feature. The analysis process for complex control systems consists of proving or verifying that the designed system indeed meets certain specifications. However, both the design and analysis may be formidable due to the complexity and magnitude of the system. From an analysis perspective, the complexity of a system can be reduced by imposing a hierarchical structure and abstraction on the architectural design. Currently, model checking has been demonstrated by more and more successes. It is an effective way to verify that the construction of a complex system satisfies to the requirements of reliability and correctness. In this paper, an approach for formally analyzing distributed control systems at architectural level by applying software architecture description and model checking techniques is presented. Through study on a building comprehensive control system, it is shown that the method could improve the quality of design of distributed control systems.

    Reference
    [1]Pappas GJ, Sastry S. Towards continuous abstractions of dynamical and control systems. In: Antsaklis P, Kohn W, Nerode A,S astry S, eds. Hybrid Systems IV. Lecture Notes in Computer Science 1273, New York: Springer-Verlag, 1997. 329~341.
    [2]Clarke E, Grumberg O, Peled D. Model-Checking. MIT Press, 1999.
    [3]Holzmann GJ. The spin model checker. IEEE Trans. on Software Engineering, 1997,23(5):279~295.
    [4]McMillan K. Symbolic Model Checking. Boston: Kluwer Academic Publishers, 1993.
    [5]Magee J, Kramer J. Concurrency: State Models & Java Programs. Indianapolis: John Wiley & Sons, 1999.
    [6]Holzmann GJ. Design and Validation of Computer Protocols. Englewood Cliffs: Prentice-Hall, 1991.
    [7]Manna Z, Pnueli A. The Temporal Logic of Reactive and Concurrent Systems: Specification. New York: Springer-Verlag, 1991.
    [8]Hoare CAR. Communicating Sequential Processes. Englewood Cliffs: Prentice-Hall, 1985.
    [9]Allen R, Garlan D. A formal basis for architectural connection. ACM Trans. on Software Engineering and Methodology, 1997,6(3):213~249.
    [10]Inverardi P, Wolf AL. Formal specifications and analysis of software architectures using the chemical abstract machine model.IEEE Trans. on Software Engineering, 1995,21 (4): 100~114.
    [11]Magee J, Kramer J, Giannakopoulou D. Behaviour analysis of software architectures. In: Donohoe P, ed. Proc. of 1st Working IFIP Conf. on Software Architecture (WICSA 1). Boston: Kluwer Academic Publishers, 1999. 35~50
    [12]Garlan D, Khersonsky S, Kim JS. Model checking publish-subscribe systems. In: Ball T, Rajamani SK, eds. Proc. of the 10th SPIN Workshop: Model Checking Software. Heidelberg: Springer-Verlag, 2003. 166~180.
    [13]Inverardi P, Muccini H, Pelliccione P. Automated check of architectural models consistency using SPIN. In: Feather M, Goedicke M, eds. Proc. of the 16th IEEE Int'l Conf. on Automated Software Engineering (ASE 2001). Los Alamitos: IEEE Computer Society Press, 2001. 346~349.
    [14]Issarny V, Kloukinas C, Zarras A. Systematic aid in the development of middleware architectures. Communications of the ACM,2002, 45(6):53~58.
    [15]Bachmann F, Bass L, Chastek G, Donohoe P, Peruzzi F. The architecture based design method. Technical Report, CMU/SEI-2000-TR-001, Pittsburgh: Software Engineering Institute, Carnegie Mellon University, 2000.
    [16]Eugster P, Felber PA, Guerraoui R, Kermarrec AM. The many faces of publish/subscribe. ACM Computing Surveys, 2003,35(2):114~131.
    [17]Taylor RN, Medvidovic N, Anderson KM, Whitehead Jr. EJ, Robbins JE, Nies KA, Oreizy P, Dubrow DL. A component- and message-based architectural style for GUI software. IEEE Trans. on Software Engineering, 1996,22(6):390~406.
    [18]Dwyer MB, Avrunin GS, Corbett JC. Patterns in property specifications for finite-state verification. In: Proc. of the 21 st Int'l Conf.on Software Engineering. Los Alamitos: IEEE Computer Society Press, 1999. 411~420.
    [19]Comella-Dorda S, Gluch D, Hudak J, Lewis G, Weinstock C. Model-Based verification: Claim creation guidelines. Technical Note,CMU/SEI-2001-TN018, Pittsburgh: Software Engineering Institute, Carnegie Mellon University, 2001.
    [20]Wang Y, Wang ZY. Design and implementation of intelligent building management system based on CORBA. Computer and Digital Engineering, 2001,29(2): 16~22 (in Chinese with English abstract).
    [21]汪洋,玉振宇.基于CORBA的智能建筑管理系统IBMS的设计与实现.计算机与数字工程,2001,29(2):16~22.
    Comments
    Comments
    分享到微博
    Submit
Get Citation

汪洋,魏峻,王振宇.基于体系结构模型检查分布式控制系统.软件学报,2004,15(6):823-833

Copy
Share
Article Metrics
  • Abstract:4192
  • PDF: 5375
  • HTML: 0
  • Cited by: 0
History
  • Received:June 01,2004
You are the first2033425Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063