Towards a Combination of CafeOBJ and PAT

  • Yongxin Zhao
  • Jinsong Dong
  • Yang Liu
  • Jun Sun
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8373)


In the quest for tractable formal methods to improve the practice of software engineering, both CafeOBJ [7] and PAT [12] have made great achievements based on different formal techniques. CafeOBJ has an evident advantage in specifying concurrent systems with object-oriented methods and proving behavioral properties based on reusability of proof. However, it is difficult to be applied to automatically verify some LTL based properties which involve complex state updates and finite path of states. Conversely, PAT offers great flexibility to simulate system behaviors and support modeling checking various properties, but it is difficult to prove behavioral properties directly, the definition of which is based on the structure of contexts. In the paper, we attempt to combine the two approaches by modeling specifications and verifying properties in CafeOBJ and PAT. A keyless car system is provided to illustrate our approach.


Model Check Linear Temporal Logic Behavioral Property Linear Temporal Logic Formula Projection Operation 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Nakagawa, A.T., Sawada, T., Futatsugi, K.: CafeOBJ User’s Manual (1997)
  2. 2.
    Goguen, J., Burstall, R.: Institutions: Abstract Model Theory for Specification and Programming. Journal of the Association for Computing Machinery 39(1), 95–146 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    Diaconescu, R., Futatsugi, K., Ogata, K.: CafeOBJ: Logical Foundations and Methodologies. Journal of Computers and Artificial Intelligence 22(3-4), 257–283 (2003)MathSciNetzbMATHGoogle Scholar
  4. 4.
    Chandy, K.M., Misra, J.: Parallel Program Design: A Foundation. Addison Wesley, Reading, MA (1988)zbMATHGoogle Scholar
  5. 5.
    Futatsugi, K.: Formal Methods in CafeOBJ. In: Hu, Z., Rodríguez-Artalejo, M. (eds.) FLOPS 2002. LNCS, vol. 2441, pp. 1–20. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  6. 6.
    Iida, S., Matsumoto, M., Diaconescu, R., Futatsugi, K., Lucanu, D.: Concurrent object composition in CafeOBJ. Technical Report IS-RR-98-0009S, Japan Advanced Institue for Science and Technology (1998) (Submitted to publication)Google Scholar
  7. 7.
    Diaconescu, R., Futatsugi, K.: CafeOBJ report. AMAST Series in Computing, vol. 6. World Scientific, Singapore (1998)zbMATHGoogle Scholar
  8. 8.
    Futatsugi, K.: An Overview of OBJ2. In: Proc. of Franco-Japanese Symp. on Programming of Future Generation Computers, pp. 139C160 (1988)Google Scholar
  9. 9.
    Nissanke, N.: Real time systems. Prentice Hall series in computer science. Prentice Hall (1997)Google Scholar
  10. 10.
    Futatsugi, K., Goguen, J.A., Jouannaud, J.P., Meseguer, J.: Principles of OBJ2. In: Proceedings of the 12th ACM Symposium on Principles of Programming Languages, pp. 55–66. ACM (1985)Google Scholar
  11. 11.
    Sun, J., Liu, Y., Dong, J.S., Chen, C.: Integrating Specification and Programs for System Modeling and Verification. In: TASE, pp. 127–135 (2009)Google Scholar
  12. 12.
    Sun, J., Liu, Y., Dong, J.S., Pang, J.: PAT: Towards Flexible Verification under Fairness. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 709–714. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  13. 13.
    Liu, Y., Sun, J., Dong, J.S.: PAT 3: An EXtensible Architecture for Building Multi-domain Model Checkers. In: ISSRE, pp. 190–199. IEEE (2011)Google Scholar
  14. 14.
    Goguen, J., Winkler, T., Meseguer, J., Futatsugi, K., Jouannaud, J.P.: Introducing OBJ. In: Goguen, J., Malcolm, G. (eds.) Software Engineering with OBJ, pp. 3–167. Kluwer Academic Publishers (2000)Google Scholar
  15. 15.
    Chen, C.Q., Sun, J., Liu, Y., Dong, J.S., Zheng, M.C.: Formal modeling and validation of Stateflow diagrams. Journal of STTT 14(6), 653–671 (2012)CrossRefGoogle Scholar
  16. 16.
    Shi, L., Zhao, Y., Liu, Y., Sun, J., Dong, J.S., Qin, S.: A UTP Semantics for Communicating Processes with Shared Variables. In: Groves, L., Sun, J. (eds.) ICFEM 2013. LNCS, vol. 8144, pp. 215–230. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  17. 17.
    Sun, J., Song, S., Liu, Y.: Model Checking Hierarchical Probabilistic Systems. In: Dong, J.S., Zhu, H. (eds.) ICFEM 2010. LNCS, vol. 6447, pp. 388–403. Springer, Heidelberg (2010)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2014

Authors and Affiliations

  • Yongxin Zhao
    • 1
  • Jinsong Dong
    • 1
  • Yang Liu
    • 2
  • Jun Sun
    • 3
  1. 1.School of ComputingNational University of SingaporeSingapore
  2. 2.Nanyang Technological UniversitySingapore
  3. 3.Singapore University of Design and TechnologySingapore

Personalised recommendations