Everlasting Challenges with the OBJ Language Family

  • Shin Nakajima
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8373)


Algebraic specification languages of the OBJ family are quite flexible in providing adequate means by which to delineate software abstractions. Although originally developed in the late 1970s, these languages are applied to new problems that have arisen with emerging software-intensive systems. As an example of continuing efforts to tackle those problems, the present paper considers the application of the OBJ family language, specifically Realtime Maude, to model-based analysis of power consumption in Android smartphones. Hereby, it demonstrates that the language is powerful enough to be a basis for dealing with this new problem.


Realtime Maude Sampling Abstraction Energy Bugs Android Smartphone 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
  2. 2.
  3. 3.
    IEEE Standard 802.11, Wireless LAN Medium Access Control (MAC) and Physical Layer (PHY) Specifications (1999)Google Scholar
  4. 4.
    Agha, G., Meseguer, J., Sen, K.: PMaude: Rewrite-based Specification Language forf Probabilistic Object Systems. ENTCS 153, 213–239 (2006)Google Scholar
  5. 5.
    Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P.-H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The Algorithmic Analysis of Hybrid Systems. Theor. Comp. Sci. (138), 3–24 (1995)Google Scholar
  6. 6.
    Alur, R.: Formal Verification of Hybrid Systems. In: Proc. EMSOFT 2011, pp. 273–278 (2011)Google Scholar
  7. 7.
    Bouyer, P., Fahrenberg, U., Larsen, K.G., Markey, N.: Quantative Analysis of Real-Time Systems Using Priced Timed Automata. Comm. ACM 54(9), 78–87 (2011)CrossRefGoogle Scholar
  8. 8.
    Brekling, A., Hansen, M.R., Madsen, J.: MoVES – A Framework for Modeling and Verifying Embedded Systems. In: Proc. ICM 2009, pp. 149–152 (2009)Google Scholar
  9. 9.
    Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007)zbMATHGoogle Scholar
  10. 10.
    David, A., Illum, J., Larsen, K.G., Skou, A.: Model-based Framework for Schedulability Analysis Using UPPAAL 4.1, Aalborg University (2009)Google Scholar
  11. 11.
    Diaconescu, R., Futatsugi, K.: CafeOBJ Report. World Scientific (1998)Google Scholar
  12. 12.
    Futatsugi, K., Goguen, J., Jouannaud, J.-P., Meseguer, J.: Principles of OBJ2. In: Proc. 12th POPL, pp. 52–66 (1985)Google Scholar
  13. 13.
    Ghezzi, C.: Adaptive Software – the fading boundary between development time and run time. An invited Talk at SEAMS 2011, Waikiki (May 2011)Google Scholar
  14. 14.
    Goguen, J., Malcolm, G.: Algebraic Semantics of Imperative Programs. The MIT Press (1996)Google Scholar
  15. 15.
    Hennessy, J.L., Patterson, D.A.: Computer Architecture: A Quantitative Approach, 5th edn. Morgan Kaufmann (2011)Google Scholar
  16. 16.
    Hiroshige, T.: History of Physics, Baihukan, vol. 1 (1968) (in Japanese)Google Scholar
  17. 17.
    Kephart, J., Chess, D.: The Vision of Autonomic Computing. IEEE Computer 36(1), 41–50 (2003)CrossRefGoogle Scholar
  18. 18.
    Manweiler, J., Choudhury, R.R.: Avoiding the Rush Hours: WiFi Energy Management via Traffic Isolation. In: Proc. MobiSys 2011 (2011)Google Scholar
  19. 19.
    Meseguer, J.: Conditional Rewriting Logic as a Unified Model of Concurrency. ENTCS 96, 73–155 (1992)MathSciNetzbMATHGoogle Scholar
  20. 20.
    Nakajima, S., Futatsugi, K.: An Object-Oriented Modeling Method for Algebraic Specifications in CafeOBJ. In: Proc. ICSE 1997, pp. 34–44 (1997)Google Scholar
  21. 21.
    Nakajima, S.: Using Algebraic Specification Techniques in Development of Object-Oriented Frameworks. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM 1999, vol. II. LNCS, vol. 1709, p. 1664. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  22. 22.
    Nakajima, S.: An Algebraic Approach to Object-Oriented Software Engineering. Ph.D. Dissertation, The University of Tokyo (2000)Google Scholar
  23. 23.
    Nakajima, S., Ishiguro, M., Tanaka, K.: Rewriting Logic Approach to Modeling and Analysis of Client Behavior in Open Systems. In: Min, S.L., Pettit, R., Puschner, P., Ungerer, T. (eds.) SEUS 2010. LNCS, vol. 6399, pp. 83–94. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  24. 24.
    Nakajima, S.: An Architecture of Dynamically Adaptive PHP-based Web Applications. In: Proc. APSEC 2011, pp. 203–210 (2011)Google Scholar
  25. 25.
    Nakajima, S.: Introduction to Formal Methods – Logic-based Software Development, Ohm-sya (2012) (in Japanese)Google Scholar
  26. 26.
    Nakajima, S.: Importance Sampling of Runtime Interference. In: Proc. APSEC 2012, pp. 693–696 (2012)Google Scholar
  27. 27.
    Nakajima, S., Miwa, Y.: Soft Edge – Searching for Sciences of Software Development. Maruzen (2013) (in Japanese)Google Scholar
  28. 28.
    Nakajima, S., Ueda, Y.: Power Consumption Analysis of Smartphone Applications using UPPAAL, Orally presented at WIP session of 1st CPSNA (August 2013)Google Scholar
  29. 29.
    Nakajima, S.: Safe Substitution of Components in Self-adaptive Web Applications. To appear in Proc. APSEC 2013 (2013)Google Scholar
  30. 30.
    Ölveczky, P.C., Meseguer, J.: Semantics and Pragmatics of Real-Time Maude. Higher-Order and Symbolic Computation 20(1-2), 161–196 (2007)CrossRefzbMATHGoogle Scholar
  31. 31.
    Pathak, A., Hu, Y.C., Zhang, M.: Bootstrapping Energy Debugging on Smartphones: A First Look at Energy Bugs in Mobile Devices. In: Proc. Hotnets 2011 (2011)Google Scholar
  32. 32.
    Pathak, A., Hu, Y.C., Zhang, M.: Where is the energy spent inside my app?: Fine Grained Energy Accoutning on Smartphones with Eprof. In: Proc. EuroSys 2012 (2012)Google Scholar
  33. 33.
    Wing, J.: A Specifier’s Introduction to Formal Methods. IEEE Computer, 8–24 (1990)Google Scholar
  34. 34.
    Zuliani, P., Baier, C., Clarke, E.M.: Rare-Event Verification for Stochastic Hybrid Systems. In: Proc. HSCC 2012, pp. 217–225 (2012)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2014

Authors and Affiliations

  • Shin Nakajima
    • 1
  1. 1.National Institute of InformaticsTokyoJapan

Personalised recommendations