Abstract
In this paper, we consider extending state transition diagrams (SDs) by new features which add new events, states and transitions. The main goal is to capture when the behavior of a state transition diagram is preserved under such an extension, which we call behavioral refinement. Our behavioral semantics is based on the observable traces of input and output events. We use assume/guarantee specifications to specify both the base SD and the extensions, where assumptions limit the permitted input streams. Based on this, we formalize behavioral refinement and also determine suitable assumptions on the input for the extended SD. We argue that existing techniques for behavioral refinement are limited by only abstracting from newly added events. Instead, we generalize this to new refinement concepts based on the elimination of the added behavior on the trace level. We introduce new refinement relations and show that properties are preserved even when the new features are added.
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 subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Alfaro, L., Henzinger, T.: Interface-based design. In: Broy, M., Grünbauer, J., Harel, D., Hoare, T. (eds.) Engineering Theories of Software Intensive Systems. NATO Science Series, vol. 195, pp. 83–104. Springer, Netherlands (2005)
Blundell, C., Fisler, K., Krishnamurthi, S., Van Hentenrvck, P.: Parameterized interfaces for open system verification of product lines. In: Proceedings of the 19th International Conference on Automated Software Engineering, pp. 258–267 (September 2004)
Broy, M.: Multifunctional software systems: Structured modeling and specification of functional requirements. Sci. Comput. Program. 75, 1193–1214 (2010)
David, A., Larsen, K.G., Legay, A., Nyman, U., Wasowski, A.: Timed I/O automata: a complete specification theory for real-time systems. In: Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2010, pp. 91–100. ACM, New York (2010)
Djoko, S.D., Douence, R., Fradet, P.: Aspects preserving properties. In: Proceedings of the 2008 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, PEPM 2008, pp. 135–145. ACM, New York (2008)
Fischbein, D., Uchitel, S., Braberman, V.: A foundation for behavioural conformance in software product line architectures. In: Proceedings of the ISSTA 2006 Workshop on Role of Software Architecture for Testing and Analysis, ROSATEA 2006, pp. 39–48. ACM, New York (2006)
Klein, C., Prehofer, C., Rumpe, B.: Feature specification and refinement with state transition diagrams. In: Fourth IEEE Workshop on Feature Interactions in Telecommunications Networks and Distributed, pp. 284–297. IOS Press (1997)
Larsen, K.G., Nyman, U., Wąsowski, A.: Interface input/output automata. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 82–97. Springer, Heidelberg (2006)
Larsen, K.G., Nyman, U., Wąsowski, A.: Modal I/O automata for interface and product line theories. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 64–79. Springer, Heidelberg (2007)
Liu, J., Basu, S., Lutz, R.: Compositional model checking of software product lines using variation point obligations. Automated Software Engineering 18, 39–76 (2011)
Prehofer, C.: Plug-and-play composition of features and feature interactions with statechart diagrams. Software and Systems Modeling 3, 221–234 (2004)
Prehofer, C.: Semantic reasoning about feature composition via multiple aspect-weavings. In: Proceedings of the 5th International Conference on Generative Programming and Component Engineering, GPCE 2006, pp. 237–242. ACM, New York (2006)
Prehofer, C.: Behavioral refinement and compatibility of statechart extensions. In: Workshop on Formal Engineering approaches to Software Components and Architectures. I Electronic Notes in Theoretical Computer Science (ENTCS) (2012)
Reeve, G., Reeves, S.: Logic and refinement for charts. In: Proceedings of the 29th Australasian Computer Science Conference, ACSC 2006, vol. 48, pp. 13–23. Australian Computer Society, Inc., Darlinghurst (2006)
Rumpe, B., Klein, C.: Automata describing object behavior. In: Specification of Behavioral Semantics in Object-Oriented Information Modeling, pp. 265–286. Kluwer Academic Publishers (1996)
Scholz, P.: Incremental design of statechart specifications. Science of Computer Programming 40(1), 119–145 (2001)
Schrefl, M., Stumptner, M.: Behavior-consistent specialization of object life cycles. ACM Trans. Softw. Eng. Methodol. 11, 92–148 (2002)
Simons, A.J.H., Stannett, M.P., Bogdanov, K.E., Holcombe, W.M.L.: W.M.l.: Plug and play safely: Rules for behavioural compatibility. In: IProc. 6th IASTED Int. Conf. Software Engineering and Applications, pp. 263–268 (2002)
Stumptner, M., Schrefl, M.: Behavior consistent inheritance in UML. In: Laender, A.H.F., Liddle, S.W., Storey, V.C. (eds.) ER 2000. LNCS, vol. 1920, pp. 527–542. Springer, Heidelberg (2000)
Zhang, G., Hölzl, M.: Hila: High-level aspects for uml state machines. In: Ghosh, S. (ed.) MODELS 2009. LNCS, vol. 6002, pp. 104–118. Springer, Heidelberg (2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Prehofer, C. (2013). Assume-Guarantee Specifications of State Transition Diagrams for Behavioral Refinement. In: Johnsen, E.B., Petre, L. (eds) Integrated Formal Methods. IFM 2013. Lecture Notes in Computer Science, vol 7940. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-38613-8_3
Download citation
DOI: https://doi.org/10.1007/978-3-642-38613-8_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-38612-1
Online ISBN: 978-3-642-38613-8
eBook Packages: Computer ScienceComputer Science (R0)