Assessing the Expressivity of Formal Specification Languages

  • Natalia López
  • Manuel Núñez
  • Ismael Rodríguez
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4019)


Formal modelling languages are powerful tools to systematically represent and analyze the properties of systems. A myriad of new modelling languages, as well as extensions of existing ones, are proposed every year. We may consider that a modelling language is useful if it allows to represent the critical aspects of systems in an expressive way. In particular, we require that the modelling language allows to accurately discriminate between correct and incorrect behaviors concerning critical aspects of the model. In this paper we present a method to assess the suitability of a modelling language to define systems belonging to a specific domain. Basically, given a system, we consider alternative correct/incorrect systems and we study whether the representations provided by the studied modelling language keep the distinction between correct and incorrect as each alternative system does.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [AD94]
    Alur, R., Dill, D.: A theory of timed automata. Theoretical Computer Science 126, 183–235 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  2. [AR00]
    Astesiano, E., Reggio, G.: Formalism and method. Theoretical Computer Science 236(1-2), 3–34 (2000)zbMATHCrossRefMathSciNetGoogle Scholar
  3. [BG98]
    Bernardo, M., Gorrieri, R.: A tutorial on EMPA: A theory of concurrent processes with nondeterminism, priorities, probabilities and time. Theoretical Computer Science 202, 1–54 (1998)zbMATHCrossRefMathSciNetGoogle Scholar
  4. [BG02]
    Bravetti, M., Gorrieri, R.: The theory of interactive generalized semi-Markov processes. Theoretical Computer Science 282(1), 5–32 (2002)zbMATHCrossRefMathSciNetGoogle Scholar
  5. [BM99]
    Bottaci, L., Mresa, E.S.: Efficiency of mutation operators and selective mutation strategies: An empirical study. Software Testing, Verification and Reliability 9, 205–232 (1999)CrossRefGoogle Scholar
  6. [GSS95]
    van Glabbeek, R., Smolka, S.A., Steffen, B.: Reactive, generative and stratified models of probabilistic processes. Information and Computation 121(1), 59–80 (1995)zbMATHCrossRefMathSciNetGoogle Scholar
  7. [Ham77]
    Hamlet, R.G.: Testing programs with the aid of a compiler. IEEE Transactions on Software Engineering 3, 279–290 (1977)CrossRefGoogle Scholar
  8. [Hil96]
    Hillston, J.: A Compositional Approach to Performance Modelling. Cambridge University Press, Cambridge (1996)CrossRefGoogle Scholar
  9. [How82]
    Howden, W.E.: Weak mutation testing and completeness of test sets. IEEE Transactions on Software Engineering 8, 371–379 (1982)CrossRefGoogle Scholar
  10. [LN01]
    López, N., Núñez, M.: A testing theory for generally distributed stochastic processes. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 321–335. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  11. [NS94]
    Nicollin, X., Sifakis, J.: The algebra of timed process, ATP: Theory and application. Information and Computation 114(1), 131–178 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  12. [Zub80]
    Zuberek, W.M.: Timed Petri nets and preliminary performance evaluation. In: 7th Annual Symposium on Computer Architecture, pp. 88–96. ACM Press, New York (1980)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2006

Authors and Affiliations

  • Natalia López
    • 1
  • Manuel Núñez
    • 1
  • Ismael Rodríguez
    • 1
  1. 1.Dept. Sistemas Informáticos y ProgramaciónUniversidad Complutense de MadridMadridSpain

Personalised recommendations