Model-driven generation of runtime checks for system properties

详细信息    查看全文

• 作者：Mauro Pezzé ; Jochen Wuttke
• 关键词：Runtime verification ; Assertions ; Software design ; Development framework ; Model ; driven design
• 刊名：International Journal on Software Tools for Technology Transfer (STTT)
• 出版年：2016
• 出版时间：February 2016
• 年：2016
• 卷：18
• 期：1
• 页码：1-19
• 全文大小：2,544 KB
• 参考文献：1.Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: an overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) Proceedings of the International Workshop on the Construction and Analysis of Safe, Secure, and Interoperable Systems, CASSIS 2004, Series. Lecture Notes in Computer Science, vol. 3362, pp. 49–69. Springer, New York (2004)
  2.de Caso, G., Braberman, V., Garbervetsky, D., Uchitel, S.: Validation of contracts using enabledness preserving finite state abstractions. In: Proceedings of the 31st International Conference on Software Engineering, ICSE ’09. IEEE Computer Society, pp. 452–462 (2009)
  3.Leavens, G.T‘., Baker, A.L., Ruby, C.: JML: a notation for detailed design. In: Kiloc, H., Rumpe, B., Simmonds, I. (eds.) Behavioral Specifications of Businesses and Systems, Chapter 12, pp. 175–188. Kluwer, Boston (1999)CrossRef
  4.Meyer, B.: Object-Oriented Software Construction, 2nd edn. Prentice Hall, London (1997)MATH
  5.Rosenblum, D.S.: A practical approach to programming with assertions. IEEE Trans. Softw. Eng. 21(1), 19–31 (1995)CrossRef
  6.Allan, C., Avgustinov, P., Christensen, A.S., Hendren, L., Kuzins, S., Lhoták, O., de Moor, O., Sereni, D., Sittampalam, G., Tibble, J.: Adding trace matching with free variables to AspectJ. In: Proceedings of the 20th Annual ACM SIGPLAN Conference on Object-oriented Programming, Systems, Languages, and Applications, Series OOPSLA ’05, pp. 345–364 (Online). doi:10.​1145/​1094811.​1094839 (2005)
  7.Avgustinov, P., Tibble, J., de Moor, O.: Making trace monitors feasible. In: Proceedings of the 22nd ACM SIGPLAN Conference on Object-Oriented Programming Systems and Applications, Series OOPSLA ’07, pp. 589–608 (online). doi:10.​1145/​1297027.​1297070 (2007)
  8.Barringer, H., Rydeheard, D., Havelund, K.: Rule systems for run-time monitoring: from EAGLE to RULER. J. Logic Comput. 20(3), 675–706 (2010)CrossRef MathSciNet MATH
  9.Bodden, E., Lam, P., Hendren, L.: Clara: a framework for partially evaluating finite-state runtime monitors ahead of time. In: Proceedings of the First International Conference on Runtime Verification ’10. Springer, Berlin, pp. 183–197. doi:10.​1007/​978-3-642-16612-9_​15 (2010)
  10.Chen, F., Roşu, G.: MOP: an efficient and generic runtime verification framework. In: Proceedings of the 22nd ACM SIGPLAN Conference on Object-Oriented Programming Systems and Applications, OOPSLA ’07. ACM, pp. 569–588 (2007)
  11.Drusinsky, D., Shing, M.-T.: Using UML statecharts with knowledge logic guards. In: Schürr, A., Selic, B. (eds.) Model Driven Engineering Languages and Systems, Series Lecture Notes in Computer Science, vol. 5795, pp. 586–590. Springer, Berlin (2009). doi:10.​1007/​978-3-642-04425-0_​45 CrossRef
  12.Havelund, K., Roşu, G.: Monitoring Java programs with Java PathExplorer. Electron. Notes Theor. Comput. Sci. 55(2), 200–217 (2001)CrossRef
  13.Meredith, P., Jin, D., Chen, F., Roşu, G.: Efficient monitoring of parametric context-free patterns. J Autom. Softw. Eng. 17(2), 149–180 (2010)CrossRef
  14.Dzidek, W.J., Briand, L.C., Labiche, Y.: Lessons learned from developing a dynamic OCL constraint enforcement tool for Java. In: Satellite Events at the MoDELS 2005 Conference, Series Lecture Notes in Computer Science, vol. 3844. Springer, Berlin, pp 10–19 (2005)
  15.Luckham, D.C., Kerry, J.J., Augustin, L.M., Vare, J., Bryan, D., Mann, W.: Specification and analysis of system architecture using Rapide. IEEE Trans. Softw. Eng. 21(4), 336–355 (1995)CrossRef
  16.Stirewalt, K., Rugaber, S.: Automated invariant maintenance via OCL compilation. In: Proceedings of the 8th International Conference on Model Driven Engineering Languages and Systems, MODELS 2005. Springer, Berlin, pp. 616–632 (2005)
  17.Wang, K., Shen, W.: Runtime checking of UML association-related constraints. In: Proceedings of the 5th International Workshop on Dynamic Analysis, WODA ’07. IEEE Computer Society (2007)
  18.Ciupa, I., Meyer, B., Oriol, M., Pretschner, A.: Finding faults: manual testing vs. random testing + vs. user reports. In: Technical Report, vol. 595. Department of Computer Science, ETH Zurich (2008)
  19.Voas, J.M., Miller, K.W.: Putting assertions in their place. In: Proceedings of the 5th International Symposium on Software Reliability Engineering, ISSRE’ 94, pp. 152–157 (1994)
  20.Pike, L., Niller, S., Wegmann, N.: Runtime verification for ultra-critical systems. In: Khurshid, S., Sen, K. (eds.) Runtime Verification, Series Lecture Notes in Computer Science, vol. 7186, pp. 310–324. Springer, Berlin (2012). doi:10.​1007/​978-3-642-29860-8_​23
  21.Wu, G., Wei, J., Ye, C., Shao, X., Zhong, H., Huang, T.: Runtime verification of data-centric properties in service based systems. In: Khurshid, S., Sen, K. (eds.) Runtime Verification, Series Lecture Notes in Computer Science, vol. 7186, pp. 325–341. Springer, Berlin (2012). doi:10.​1007/​978-3-642-29860-8_​24
  22.Goldsmith, S.F., O’Callahan, R., Aiken, A.: Relational queries over program traces. In: Proceedings of the 20th ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, Series OOPSLA ’05, pp. 385–402 (online). doi:10.​1145/​1094811.​1094841 (2005)
  23.Martin, M., Livshits, B., Lam, M.S.: Finding application errors and security flaws using PQL: a program query language. In: Proceedings of the 20th ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, Series OOPSLA ’05, ACM, New York, pp. 365–383 (online). doi:10.​1145/​1094811.​1094840 (2005)
  24.Chen, F., d’Amorim, M., Roşu, G.: Checking and correcting behaviors of Java programs at runtime with Java-MOP. Electron. Notes Theor. Comput.Sci. 144(4), 3–20 (2006) (online). http://​www.​sciencedirect.​com/​science/​article/​pii/​S157106610600300​8
  25.Kim, M., Viswanathan, M., Kannan, S., Lee, I., Sokolsky, O.: Java-MaC: a run-time assurance approach for Java programs. Formal Methods Syst. Des. 24, 129–155 (2004)CrossRef MATH
  26.The Object Management Group: OMG Unified Modeling Language Superstructure. (adopted specification formal/2007-11-02, http://​www.​omg.​org ). Accessed 02 Jan 2008 (2007)
  27.The Object Management Group: Object Constraint Language (available specification formal/06-05-01, http://​www.​omg.​org ). Accessed 11 Dec 2006 (2005)
  28.Hein, C., Ritter, T., Wagner, M.: System monitoring using constraint checking as part of model based system management. In: 2nd International Workshop on Models@run.time (2007)
  29.Richters, M., Gogolla, M.: Aspect-oriented monitoring of UML and OCL constraints. In: AOSD Modeling with UML Workshop at the 6th International Conference on the Unified Modeling Language (UML) (2003)
  30.Aldrich, J., Chambers, C., Notkin, D.: ArchJava: connecting software architecture to implementation. In: Proceedings of the 24th International Conference on Software Engineering, ICSE ’02. ACM, pp. 187–197 (2002)
  31.Taylor, R.N., Medvidovic, N., Dashofy, E.: Software Architecture: Foundations, Theory, and Practice. Wiley, New York (2009)CrossRef
  32.Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley Professional, New York (1994)
  33.Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: ICSE 1999: Proceedings of the 1999 International Conference on Software Engineering, pp. 411–420 (1999)
  34.Cobleigh, R.L., Avrunin, G.S., Clarke, L.A.: User guidance for creating precise and accessible property specifications. In: FSE-14: Proceedings of the 14th ACM SIGSOFT International Symposium on Foundations of Software Engineering, pp. 208–218 (2006)
  35.Wuttke, J.: Property templates and assertions supporting runtime failure detection. In: Technical Report, University of Lugano, Switzerland, 04 Aug 2008 (2008)
  36.Wuttke, J.: Automatically generated runtime checks for design-level properties. Ph.D. dissertation, University of Lugano, Lugano (2010)
  37.Laddad, R.: AspectJ in Action: Enterprise AOP with Spring, 2nd edn. Manning Publications, New York (2009)
  38.Gorla, A., Pezzé, M., Wuttke, J., Mariani, L., Pastore, F.: Achieving cost-effective software reliability through self-healing. Comput. Inform. 2(1), 1001–1022 (2010)
  39.Denaro, G., Gorla, A., Pezzè, M.: Datec: dataflow testing of Java classes. In: 31st International Conference on Software Engineering, ICSE’09—Companion Volume. IEEE Computer Society, pp. 421–422 (tool demonstration) (2009)
  40.Lee, C., Jin, D., Meredith, P.O., Rosu, G.: Towards categorizing and formalizing the JDK API. In: Technical Report, University of Illinois (online). http://​hdl.​handle.​net/​2142/​30006 (2012)
  41.Java Server Pages 2.1 Specification. http://​jcp.​org/​en/​jsr/​detail?​id=​245 (JSR 245). Accessed Jan 2008 (2006)
  42.Unkel, C., Lam, M.S.: Automatic inference of stationary fields: a generalization of Java’s final fields. In: Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’08. ACM, pp. 183–195 (2008)
  43.The Objective-C 2.0 Programming Language. Apple Inc., Cupertino (2008)
  44.König, D.: Groovy in Action. Manning Publications, New York (2007)
  
• 作者单位：Mauro Pezzé (1) (2)
  Jochen Wuttke (3)
  
  1. University of Lugano, Lugano, Switzerland
  2. University of Milano Bicocca, Milan, Italy
  3. University of Washington, Seattle, USA
  
• 刊物类别：Computer Science
• 刊物主题：Software Engineering
  Software Engineering, Programming and Operating Systems
  Theory of Computation
  
• 出版者：Springer Berlin / Heidelberg
• ISSN：1433-2787

文摘

Creating runtime monitors for interesting properties is an important research problem. Existing approaches to runtime verification require specifications that not only define the property to monitor, but also contain details of the implementation, sometimes even requiring the implementation to add special variables or methods for monitoring. Often intuitive properties such as “event X should only happen when objects A and B agree” have to be translated by developers into complex specifications, for example, pre- and post-conditions on several methods that only in concert express this simple property. In most specification languages, the result of this manual translation are specifications that are so strongly tailored to the program at hand and the objects involved that, even if the property occurs again in a similar program, the whole translation process has to be repeated to create a new specification. In this paper, we introduce the concept of property templates. Property templates are pre-defined constraints that can be easily reused in specifications. They are part of a model-driven framework that translates high-level specifications into runtime monitors specialized to the problem at hand. The framework is extensible: Developers can define property templates for constraints they often need and can specialize the code generation when the default implementation is not satisfactory. We demonstrate the use of the framework in some case studies using a set of functional and structural constraints that we developed through an extensive study of existing software specifications. The key innovations of the approach we present are three. First, the properties developed with this approach are reusable and apply to a wide range of software systems, rather than being ad hoc and tailored to one particular program. Second, the properties are defined at a relatively high level of abstraction, so that no detailed knowledge of the implementation is needed to decide whether a given property applies. Third, we separate the definition of precise assertions for properties, and the use of properties. That way, experts can determine which assertions are needed to assure properties, and other developers can easily use these definitions to annotate systems. Keywords Runtime verification Assertions Software design Development framework Model-driven design