Specifying and Composing Non-functional Requirements in Model-Based Development

  • Ethan K. Jackson
  • Dirk Seifert
  • Markus Dahlweid
  • Thomas Santen
  • Nikolaj Bjørner
  • Wolfram Schulte
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5634)


Non-functional requirements encompass important design concerns such as schedulability, security, and communication constraints. In model-based development they non-locally impact admissible platform-mappings and design spaces. In this paper we present a novel and formal approach for specifying non-functional requirements as con straint-systems over the space of models. Our approach, based on structured logic programming, allows interacting requirements to be specified independently from each other and composed together. Correct-by- construction operators eliminate some composition mistakes. Our approach is implemented in our formal modeling tool FORMULA, which can analyze the impacts of interacting non-functional requirements on platform mappings and design spaces.


Logic Program Composition Operator Logic Programming Software Product Line Platform Model 
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.
    Jackson, M., Zave, P.: Domain descriptions. In: Proceedings of IEEE International Symposium Requirements Engineering (RE), pp. 56–64 (January 1993)Google Scholar
  2. 2.
    Pinto, A., Bonivento, A., Sangiovanni-Vincentelli, A.L., Passerone, R., Sgroi, M.: System level design paradigms: Platform-based design and communication synthesis. ACM Trans. Design Autom. Electr. Syst. 11(3), 537–563 (2006)CrossRefGoogle Scholar
  3. 3.
    Karsai, G., Sztipanovits, J., Lédeczi, Á., Bapty, T.: Model-integrated development of embedded software. Proceedings of the IEEE 91(1), 145–164 (2003)CrossRefGoogle Scholar
  4. 4.
    Lee, E.A., Xiong, Y.: A behavioral type system and its application in Ptolemy II. Formal Asp. Comput. 16(3), 210–237 (2004)CrossRefzbMATHGoogle Scholar
  5. 5.
    Henzinger, T.A., Sifakis, J.: The Embedded Systems Design Challenge. In: Proceedings of the International Symposium on Formal Methods (FM), pp. 1–15 (2006)Google Scholar
  6. 6.
    Sprinkle, J., Karsai, G.: A domain-specific visual language for domain model evolution. J. Vis. Lang. Comput. 15(3-4), 291–307 (2004)CrossRefGoogle Scholar
  7. 7.
    Chen, K., Sztipanovits, J., Neema, S.: Compositional specification of behavioral semantics. In: Proceedings of Design, Automation and Test in Europe Conference (DATE), pp. 906–911 (2007)Google Scholar
  8. 8.
    Bliudze, S., Sifakis, J.: A Notion of Glue Expressiveness for Component-Based Systems. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 508–522. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  9. 9.
    Jackson, E., Schulte, W., Sztipanovits, J.: The Power of Rich Syntax for Model-based Development. Technical Report MSR-TR-2008-86, Microsoft Research (June 2008)Google Scholar
  10. 10.
    Benveniste, A., Caillaud, B., Carloni, L.P., Caspi, P., Sangiovanni-Vincentelli, A.L.: Composing heterogeneous reactive systems. ACM Trans. Embedded Comput. Syst. 7(4) (2008)Google Scholar
  11. 11.
    Czarnecki, K., Helsen, S.: Classification of Model Transformation Approaches. In: Workshop on Generative Techniques in the Context of Model-Driven Architecture (OOPSLA), pp. 1–17 (2003)Google Scholar
  12. 12.
    Balarin, F., Watanabe, Y., Hsieh, H., Lavagno, L., Passerone, C., Sangiovanni-Vincentelli, A.L.: Metropolis: An Integrated Electronic System Design Environment. IEEE Computer 36(4), 45–52 (2003)CrossRefGoogle Scholar
  13. 13.
    Weisemöller, I., Schürr, A.: Formal Definition of MOF 2.0 Metamodel Components and Composition. In: Proceedings of the Model Driven Engineering Languages and Systems, pp. 386–400 (2008)Google Scholar
  14. 14.
    Neema, S., Sztipanovits, J., Karsai, G., Butts, K.: Constraint-Based Design-Space Exploration and Model Synthesis. In: Proceedings of the International Conference on Embedded Software (EMOFT), pp. 290–305 (2003)Google Scholar
  15. 15.
    Czarnecki, K., Wasowski, A.: Feature Diagrams and Logics: There and Back Again. In: Proceedings of the International Conference on Software Product Lines (SPLC), pp. 23–34 (2007)Google Scholar
  16. 16.
    Dantsin, E., Voronkov, A.: Expressive Power and Data Complexity of Query Languages for Trees and Lists. In: Proceedings of the Symposium on Principles of Database Systems (PODS), pp. 157–165 (2000)Google Scholar
  17. 17.
    de Moura, L.M., Bjørner, N.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  18. 18.
    Jackson, D.: Alloy: A New Technology for Software Modelling. In: Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems, p. 20 (2002)Google Scholar
  19. 19.
    Object Management Group: Mda guide version 1.0.1. Technical report (2003)Google Scholar
  20. 20.
    Henzinger, T.A., Horowitz, B., Kirsch, C.M.: Giotto: a time-triggered language for embedded programming. Proceedings of the IEEE 91(1), 84–99 (2003)CrossRefzbMATHGoogle Scholar
  21. 21.
    Kopetz, H., Bauer, G.: The time-triggered architecture. Proceedings of the IEEE 91(1), 112–126 (2003)CrossRefGoogle Scholar
  22. 22.
    Pree, W., Templ, J.: Modeling with the Timing Definition Language (TDL). In: Broy, M., Krüger, I.H., Meisinger, M. (eds.) ASWSD 2006. LNCS, vol. 4922, pp. 133–144. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  23. 23.
    Gurevich, Y., Neeman, I.: DKAL: Distributed-Knowledge Authorization Language. In: 21st IEEE Computer Security Foundations Symposium (CSF), pp. 149–162 (2008)Google Scholar
  24. 24.
    Becker, M.Y., Fournet, C., Gordon, A.D.: Design and Semantics of a Decentralized Authorization Language. In: 20th IEEE Computer Security Foundations Symposium, pp. 3–15 (2007)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Ethan K. Jackson
    • 1
  • Dirk Seifert
    • 2
  • Markus Dahlweid
    • 2
  • Thomas Santen
    • 2
  • Nikolaj Bjørner
    • 1
  • Wolfram Schulte
    • 1
  1. 1.Microsoft ResearchRedmond
  2. 2.European Microsoft Innovation CenterAachenGermany

Personalised recommendations