Abstract
Designing software subject to uncertainty in a way that provides guarantees about its run-time behavior while achieving an acceptable balance between multiple extra-functional properties is still an open problem. Tools and techniques to inform engineers about poorly-understood design spaces in the presence of uncertainty are needed. To tackle this problem, we propose an approach that combines synthesis of spaces of system design alternatives from formal specifications of architectural styles with probabilistic formal verification. The main contribution of this paper is a formal framework for specification-driven synthesis and analysis of design spaces that provides formal guarantees about the correctness of system behaviors and satisfies quantitative properties (e.g., defined over system qualities) subject to uncertainty, which is factored as a first-class entity.
Keywords
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsNotes
- 1.
Although the notion of behavioral type is more general [21], we employ the term to refer to an abstract state machine specification capturing the behavior of an architectural abstract type.
- 2.
The semantics of behavioral types are inspired by discrete-time Markov chains, so the original probability of the transition prob(t) is divided equally among transition instances.
References
Aleti, A., Bjornander, S., Grunske, L., Meedeniya, I.: Archeopterix: an extendable tool for architecture optimization of AADL models. In: ICSE Workshop on Model-Based Methodologies for Pervasive and Embedded Software, MOMPES 2009 (2009)
Bagheri, H., Malek, S.: Titanium: efficient analysis of evolving alloy specifications. In: Proceedings of the 24th Symposium on Foundations of Software Engineering, FSE 2016 (2016)
Bagheri, H., Sullivan, K.J.: Model-driven synthesis of formally precise, stylized software architectures. Formal Asp. Comput. 28(3), 441–467 (2016)
Bagheri, H., Tang, C., Sullivan, K.J.: Trademaker: automated dynamic analysis of synthesized tradespaces. In: 36th International Conference on Software Engineering. ACM (2014)
Bondarev, E., Chaudron, M.R.V., de Kock, E.A.: Exploring performance trade-offs of a jpeg decoder using the deepcompass framework. In: 6th WS on Software and Performance, WOSP. ACM (2007)
Cámara, J., Garlan, D., Schmerl, B., Pandey, A.: Optimal planning for architecture-based self-adaptation via model checking of stochastic games. In: 30th ACM Symposium on Applied Computing (SAC) (2015)
Dwivedi, V., Garlan, D., Pfeffer, J., Schmerl, B.: Model-based assistance for making time/fidelity trade-offs in component compositions. In: 11th International Conference on Information Technology: New Generations, ITNG 2014. IEEE CS (2014)
Garlan, D.: Software engineering in an uncertain world. In: Proceedings of the Workshop on Future of Software Engineering Research, FoSER (2010)
Garlan, D., Monroe, R.T., Wile, D.: Acme: an architecture description interchange language. In: Proceedings of the 1997 Conference of the Centre for Advanced Studies on Collaborative Research, Toronto, Ontario, Canada, 10–13 November 1997. IBM (1997)
Hahn, E.M., Hermanns, H., Wachter, B., Zhang, L.: PARAM: a model checker for parametric markov models. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 660–664. Springer, Heidelberg (2010). doi:10.1007/978-3-642-14295-6_56
Jackson, D.: Alloy: a lightweight object modelling notation. ACM Trans. Softw. Eng. Methodol. 11(2), 256–290 (2002)
Johnson, K., Calinescu, R., Kikuchi, S.: An incremental verification framework for component-based software systems. In: Proceedings of the 16th International ACM SIGSOFT Symposium on Component-based Software Engineering, CBSE 2013. ACM (2013)
Kang, E., Milicevic, A., Jackson, D.: Multi-representational security analysis. In: Proceedings of the 24th Symposium on Foundations of Software Engineering, FSE (2016)
Kim, J., Garlan, D.: Analyzing architectural styles. J. Syst. Softw. 83(7), 1216–1235 (2010)
Kwiatkowska, M., Norman, G., Parker, D.: Stochastic model checking. In: Bernardo, M., Hillston, J. (eds.) SFM 2007. LNCS, vol. 4486, pp. 220–270. Springer, Heidelberg (2007). doi:10.1007/978-3-540-72522-0_6
Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22110-1_47
MacCalman, A.D., Beery, P.T., Paulo, E.P.: A systems design exploration approach that illuminates tradespaces using statistical experimental designs. Syst. Eng. 19(5), 409–421 (2016)
Mahdavi-Hezavehi, S., Galster, M., Avgeriou, P.: Variability in quality attributes of service-based software systems: a systematic literature review. Inf. Softw. Technol. 55(2), 320–343 (2013)
Maoz, S., Ringert, J.O., Rumpe, B.: Synthesis of component and connector models from crosscutting structural views. In: European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2013. ACM (2013)
Martens, A., Koziolek, H., Becker, S., Reussner, R.: Automatically improve software architecture models for performance, reliability, and cost using evolutionary algorithms. In: International Conference on Performance Engineering, WOSP/SIPEW. ACM (2010)
Maydl, W., Grunske, L.: Behavioral types for embedded software – a survey. In: Atkinson, C., Bunse, C., Gross, H.-G., Peper, C. (eds.) Component-Based Software Development for Embedded Systems. LNCS, vol. 3778, pp. 82–106. Springer, Heidelberg (2005). doi:10.1007/11591962_5
Quigley, M., Conley, K., Gerkey, B.P., Faust, J., Foote, T., Leibs, J., Wheeler, R., Ng, A.Y.: Ros: an open-source robot operating system. In: ICRA WS on Open Source Software (2009)
Shaw, M., Garlan, D.: Software Architecture - Perspectives on an Emerging Discipline. Prentice Hall, Upper Saddle River (1996)
Warmer, J., Kleppe, A.: The Object Constraint Language: Getting Your Models Ready for MDA. Addison-Wesley, Reading (2003)
Weyns, D., Calinescu, R.: Tele assistance: a self-adaptive service-based system exemplar. In: 10th IEEE/ACM International Symposium on Software Engineering for Adaptive and Self-Managing Systems, SEAMS 2015. IEEE Computer Society (2015)
Wong, S., Sun, J., Warren, I., Sun, J.: A scalable approach to multi-style architectural modeling and verification. In: 13th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS 2008) (2008)
Acknowledgments
This material is based on research sponsored by AFRL and DARPA under agreement number FA8750-16-2-0042. The U.S. Government is authorized to reproduce and distribute reprints for Governmental purposes notwithstanding any copyright notation thereon. The views and conclusions contained herein are those of the authors and should not be interpreted as necessarily representing the official policies or endorsements, either expressed or implied, of the AFRL, DARPA or the U.S. Government.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Cámara, J., Garlan, D., Schmerl, B. (2017). Synthesis and Quantitative Verification of Tradeoff Spaces for Families of Software Systems. In: Lopes, A., de Lemos, R. (eds) Software Architecture. ECSA 2017. Lecture Notes in Computer Science(), vol 10475. Springer, Cham. https://doi.org/10.1007/978-3-319-65831-5_1
Download citation
DOI: https://doi.org/10.1007/978-3-319-65831-5_1
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-65830-8
Online ISBN: 978-3-319-65831-5
eBook Packages: Computer ScienceComputer Science (R0)