We use cookies to improve your experience with our site.

Indexed in:

SCIE, EI, Scopus, INSPEC, DBLP, CSCD, etc.

Submission System
(Author / Reviewer / Editor)
Advanced Search
Volume 25 Issue 6
October  2010
Turn off MathJax
Article Contents
Abstract
References
Related Articles
Xu-Tao Du, Chun-Xiao Xing, Li-Zhu Zhou. Modeling and Verifying Concurrent Programs with Finite Chu Spaces[J]. Journal of Computer Science and Technology, 2010, 25(6): 1168-1183. DOI: 10.1007/s11390-010-1093-4
Citation: Xu-Tao Du, Chun-Xiao Xing, Li-Zhu Zhou. Modeling and Verifying Concurrent Programs with Finite Chu Spaces[J]. Journal of Computer Science and Technology, 2010, 25(6): 1168-1183. DOI: 10.1007/s11390-010-1093-4
shu

Modeling and Verifying Concurrent Programs with Finite Chu Spaces

  • 1. Department of Computer Science and Technology, Tsinghua University, Beijing 100084, China;
    2. Research Institute of Information Technology, Tsinghua University, Beijing 100084, China

Funds: This work is supported by the National High-Tech Research and Development 863 Program of China under Grant No. 2009AA01Z143, and the Research Foundation of the Ministry of Railways and Tsinghua University under Grant No. J2008X009.
More Information
  • Author Bio:

    Xu-Tao Du is currently a Ph.D. candidate in the Department ofComputer Science and Technology, Tsinghua University, China.His primary research interest is in the area of formal semantics ofprogramming languages, process algebra, formal methods in softwareverification and uncertainty analysis.

    Chun-Xiao Xing is a professor at the Research Institute of Information Technology,Tsinghua University, China.He received the Ph.D. degree from the Department of Automatic Control,Northwestern Polytechnical University, Xi'an, China.His research interests include data-driven systems, digital library systems and e-commerce.He is a member of the CCF and IEEE.

    Li-Zhu Zhou is a professor at the Department of Computer Science and Technology,Tsinghua University, China.His areas of research interest include high confidence software, database systems,search engines and data mining.He is a member of the ACM.

  • Received Date: July 14, 2009
  • Revised Date: January 26, 2010
  • Published Date: October 31, 2010
    Abstract
  • Finite Chu spaces are proposed for the modeling and verification of concurrent programs. In order to model not only typical concurrent behaviors but also modern exception handling and synchronization mechanisms, we design an enriched process algebra of Chu spaces from a practical point of view. To illustrate the power of finite Chu spaces and the process algebra while abstracting away from language-specific details, an imaginary concurrent programming language (ICL) is designed. A denotational semantics of ICL is presented using finite Chu spaces and the enriched process algebra. The valuation functions are fairly straightforward since the carefully designed operators have done much of the job. The enriched process algebra is also used as the specification language for Chu spaces, with which process-algebraic properties can be specified. Verification algorithms are presented with their time complexities discussed.
    • FullText(HTML)
    • References (30)
  • [1]
    Barr M. *-Autonomous categories. Lecture Notes in Mathematics, vol. 752, Springer-Verlag, 1979.
    [2]
    Gupta V, Pratt V R. Gates accept concurrent behavior. In Proc. the 34th Annual Symposium on Foundations of Computer Science (FOCS 1993), Palo Alto, USA, Nov. 3-5, 1993, pp.62-71.
    [3]
    Pratt V R. Time and information in sequential and concurrent computation. In Proc. the International Workshop on Theory and Practice of Parallel Programming (TPPP 1994), Sendai, Japan, Nov. 7-9, 1994, pp.1-24.
    [4]
    Pratt V R. Chu Spaces and Their Interpretation as Concurrent Objects. Computer Science Today: Recent Trends and Developments, J van Leeuwen (ed.), Springer Berlin/Heidelberg, 1995, pp.392-405.
    [5]
    Pratt V R. Rational mechanisms and natural mathematics. In Proc. the 6th International Joint Conference CAAP/FASE on Theory and Practice of Software Development (TAPSOFT 1995), Aarhus, Denmark, May 22-26, 1995, pp.108-122.
    [6]
    Pratt V R. Chu spaces: Course notes for the school in category theory and applications. Coimbra, Portugal, July 1999, http://boole.stanford.edu/pub/coimbra.pdf.
    [7]
    Vannucci S. Game formats as Chu spaces. International Game Theory Review (IGTR), 2007, 9(1): 119-138.
    [8]
    Droste M, Zhang G Q. Bifinite Chu spaces. In Proc. the Second International Conference on Algebra and Coalgebra in Computer Science (CALCO 2007), Bergen, Norway, Aug. 20-24, 2007, pp.179-193.
    [9]
    Huang F P, Droste M, Zhang G Q. A monoidal category of bifinite Chu spaces. Electron. Notes Theor. Comput. Sci., April 2008, 212: 285-297.
    [10]
    Pratt V R. Chu spaces as a semantic bridge between linear logic and mathematics. Theor. Comput. Sci., 2003, 294(3): 439-471.
    [11]
    Pratt V R. Event-state duality: The enriched case. In Proc. the 13th International Conference on Concurrency Theory (CONCUR 2002), Brno, Czech, Aug. 20-23, 2002, pp.41-56.
    [12]
    Devarajan H, Hughes D J D, Plotkin G D, Pratt V R. Full completeness of the multiplicative linear logic of Chu spaces. In Proc. the 14th Annual IEEE Symposium on Logic in Computer Science (LICS 1999), Trento, Italy, July 2-5, 1999, pp.234-242.
    [13]
    Giuli E, Tholen W. A topologist's view of Chu spaces. Electron. Notes Theor. Comput. Sci., 15(5/6): 573-598.
    [14]
    Chen X, Li Q, Deng Z. Formal topology, Chu space and approximable concept. In Proc. the International Workshop on Concept Lattices and Their Applications (CLA 2005), Olomouc, Czech, Sept. 7-9 2005, pp.158-165.
    [15]
    Nguyen H T, Kreinovich V, Wu B. Chu spaces --- A new approach to diagnostic information fusion. In Proc. the 2nd International Conference on Information Fusion (FUSION 1999), Sunnyvale, USA, July 6-8, 1999, pp.323-330.
    [16]
    Nguyen N, Nguyen H T, Wu B, Kreinovich V. Chu spaces: Towards new foundations for fuzzy logic and fuzzy control, with applications to information flow on the world wide web. JACIII, 2001, 5(3): 149-156.
    [17]
    Kreinovich V, Liu G, Nguyen H. Chu spaces --- A new approach to describing uncertainty in systems. In Proc. the 42nd Midwest Symposium on Circuits and Systems, Las Cruces, USA, Aug. 8-11, 1999, pp.427-430.
    [18]
    Chen X, Li Q, Deng Z. Chu space and approximable concept lattice in fuzzy setting. In Proc. the 2007 IEEE International Conference on Fuzzy Systems (ICFS 2007), London, UK, July 23-26, 2007, pp.1-6.
    [19]
    Abramsky S. Big toy models: Representing physical systems as Chu spaces. OUCL, Tech. Rep. RR-09-08, Sept. 2009.
    [20]
    Abramsky S. Coalgebras, Chu spaces, and representations of physical systems. OUCL, Tech. Rep. RR-09-11, Oct. 2009.
    [21]
    Sato K, Horiuchi T, Hiraoka T, Kawakami H, Katai O. Decision making process via constraint-oriented fuzzy logic based on Chu space theory. In Proc. the Ninth IEEE International Conference on Fuzzy Systems (FUZZ 2000), San Antonio, USA, May 7-10, 2000, pp.222-227.
    [22]
    Vinh J, Bowen P C. Semantics of RTL and validation of synthesized RTL designs using formal verification in reconfigurable computing systems. In Proc. the 12th IEEE International Conference and Workshops on the Engineering of Computer-Based Systems (ECBS 2005), Greenbelt, USA, April 4-7, 2005, pp.247-254.
    [23]
    Ivanov L. Modeling non-iterated system behavior with Chu spaces. In Proc. the 2008 International Conference on Computer Design (CDES 2008), Las Vegas, USA, July 14-17, 2008, pp.145-150.
    [24]
    Pratt V R. Transition and cancellation in concurrency and branching time. Math. Structures in Comp. Sci., Aug. 2003, 13(4): 485-529.
    [25]
    Gupta V. Chu spaces: A model of concurrency
    [Ph.D. Dissertation]. Stanford University, Sept. 1994.
    [26]
    Web services business process execution language version 2.0. OASIS Web Services Business Process Execution Language (WSBPEL) Technical Committee, April 2007, http://www.oasis-open.org/specs/index.php#wsbpel.
    [27]
    Wing J. Hints to specifiers. Educational Issues of Formal Methods, Hinchey M, Dean N (eds.), Ch. 5, London: Academic Press, 1996, pp.57-77.
    [28]
    Du X, Xing C, Zhou L. A Chu spaces semantics of BPEL-like fault handling. In Proc. The 4th International Conference on Frontier of Computer Science and Technology (FCST 2009), Shanghai, China, Dec. 17-19, 2009, pp.317-323.
    [29]
    Du X, Xing C, Zhou L. A Chu spaces semantics of control flow in BPEL. In Proc. 2009 Asia-Pacific Services Computing Conference (APSCC 2009), Singapore, Dec. 7-11, 2009, pp.142-149.
    [30]
    de Medeiros A A, van der Aalst W, Weijters A. Quantifying process equivalence based on observed behavior. Data & Knowledge Engineering, 2008, 64(1): 55-74.
    • Relative Articles

  • Related Articles

    [1]Jeff Huang, Charles Zhang. Debugging Concurrent Software: Advances and Challenges[J]. Journal of Computer Science and Technology, 2016, 31(5): 861-868. DOI: 10.1007/s11390-016-1669-8
    [2]Lei Zhao, Ji-Wen Yang. Resources Snapshot Model for Concurrent Transactions in Multi-Core Processors[J]. Journal of Computer Science and Technology, 2013, 28(1): 106-118. DOI: 10.1007/s11390-013-1315-7
    [3]Zhen-Hua Duan, Maciej Koutny. A Framed Temporal Logic Programming Language[J]. Journal of Computer Science and Technology, 2004, 19(3).
    [4]YU Jian, WANG Shengyuan, YUAN Chongyi. Solving Inheritance Anomaly with OMNets[J]. Journal of Computer Science and Technology, 2002, 17(1).
    [5]LI Li. Towards a Denotational Semantics of Timed RSL Using Duration Calculus[J]. Journal of Computer Science and Technology, 2001, 16(1).
    [6]Qu Yunyao, Tian Zengping, Wang Yuun, Shi Baile. Design and Implementation of a Concurrency Control Mechanism in an Object-Oriented Database System[J]. Journal of Computer Science and Technology, 1996, 11(4): 337-246.
    [7]Qu Yuzhong, Wang Zhijian, Xu Jiafu. Denotational Semantics of a Simple Model of Eiffel[J]. Journal of Computer Science and Technology, 1995, 10(3): 214-226.
    [8]Zhou Jianqiang, Xie Li, Sun Zhongxiu, Zhu Genjiang. An Adaptive Strategy Integrating Locking with Optimistic Concurrency Control[J]. Journal of Computer Science and Technology, 1993, 8(4): 61-69.
    [9]Xu Qingyun, Wang Nengbin. Concurrency Control Mechanism of Complex Objects[J]. Journal of Computer Science and Technology, 1992, 7(4): 305-310.
    [10]Zhao Xudong, Feng Yulin. Automatic and Hierarchical Verification for Concurrent Systems[J]. Journal of Computer Science and Technology, 1990, 5(3): 241-249.
    • Supplements (0)

Catalog

    Get Citation
    PDF
    XML
    Article views (32) PDF downloads (2083) Cited by()
    Related

    Copyright ©2025 JCST, All Rights Reserved     京ICP备05002829号-1

    Institute of Computing Technology, Chinese Academy of Sciences
    P.O. Box 2704, Beijing 100190, P.R. China

    Tel.: 86-10-62610746 E-mail: jcst@ict.ac.cn

    /

    DownLoad:  Full-Size Img  PowerPoint
    Return
    Return