Abstract
Execution environments are used as specifications for specialization of input-output programs in the derivation of product lines. These environments, formalized as color-blind I/O-alternating transition systems, are tolerant to mutations in a given program’s outputs. Execution environments enable new compiler optimizations, vastly exceeding usual reductions. We propose a notion of context-dependent refinement for I/O-alternating transition systems, which supports composition and hierarchical reuse. The framework is demonstrated by discussing adaptations to realistic design languages and by presenting an exampleof a product line.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
de Alfaro, L., Henzinger, T.A.: Interface automata. In: Foundations of Software Engineering (FSE), Vienna, pp. 109–120. ACM Press, New York (2001)
Berry, G.: The foundations of Esterel. In: Plotkin, G., et al. (eds.) Proof, Language and Interaction. Essays in Honour of Robin Milner, pp. 425–454. MIT Press, Cambridge (2000)
Clarke, E.M.: Model Checking. The MIT Press, Cambridge (1999)
Danvy, O., et al. (eds.): Dagstuhl Seminar 1996. LNCS, vol. 1110. Springer, Heidelberg (1996)
Etalle, S., Gabbrieli, M.: Partial evaluation of concurrent constraint languages. ACM Computing Surveys 30(3es) (september 1998)
van Glabbeek, R.: The linear time–branching time spectrum. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458. Springer, Heidelberg (1990)
Harel, D.: Statecharts: A visual formalism for complex systems. Science of Computer Programming 8, 231–274 (1987)
Hatcliff, J., Mogensen, T.Æ., Thiemann, P. (eds.): DIKU 1998. LNCS, vol. 1706. Springer, Heidelberg (1999)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall, Englewood Cliffs (1985)
Hosoya, H., Kobayashi, N., Yonezawa, A.: Partial evaluation scheme for concurrent languages and its correctness. In: Bougé, L., et al. (eds.) Euro-Par 1996. LNCS, vol. 1123. Springer, Heidelberg (1996)
IAR Inc. IAR visualSTATE®, http://www.iar.com/Products/VS/
Igarashi, A., Kobayashi, N.: A generic type system for the pi-calculus. In: POPL 2001. ACM Press, New York (2001)
Jones, N.D., Gomard, C.K., Sestoft, P.: Partial Evaluation and Automatic Program Generation. Prentice Hall, Englewood Cliffs (1993)
Larsen, K.G., Milner, R.: A compositional protocol verification using relativized bisimulation. Information and Computation 99(1), 80–108 (1992)
Larsen, K.: Context Dependent Bisimulation Between Processes. PhD thesis, Edinburgh University (1986)
Larsen, K.: A context dependent equivalence between processes. Theoretical Computer Science 49, 184–215 (1987)
Lind-Nielsen, J., Andersen, H.R., Hulgaard, H., Behrmann, G., Kristoffersen, K., Larsen, K.G.: Verification of large state/event systems using compositionality and dependency analysis. Formal Methods in System Design 18(1), 5–23 (2001)
Lynch, N.: I/O automata: A model for discrete event systems. In: Annual Conference on Information Sciences and Systems, Princeton, N.J, pp. 29–38 (1988)
Milner, R.: Communication and Concurrency. Prentice Hall, Englewood Cliffs (1989)
Murakami, M.: Partial evaluation of reactive communciating processes using temporal logic formulas. In: Algebraic and Object-Oriented Approaches to Software Science (1995)
Object Management Group. OMG Unified Modelling Language specification (1999)
Rajamani, S.K., Rehof, J.: Conformance checking for models of asynchronous message passing software. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 166. Springer, Heidelberg (2002)
Scope: a statechart compiler., http://www.mini.pw.edu.pl/~wasowski/scope
Sun Microsystems, Inc. Java Card(TM) specification., http://java.sun.com/
Węsowski, A.: Automatic generation of program families by model restrictions. In: Nord, R.L. (ed.) SPLC 2004. LNCS, vol. 3154, pp. 73–89. Springer, Heidelberg (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Larsen, K.G., Larsen, U., Wasowski, A. (2005). Color-Blind Specifications for Transformations of Reactive Synchronous Programs. In: Cerioli, M. (eds) Fundamental Approaches to Software Engineering. FASE 2005. Lecture Notes in Computer Science, vol 3442. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-31984-9_13
Download citation
DOI: https://doi.org/10.1007/978-3-540-31984-9_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25420-1
Online ISBN: 978-3-540-31984-9
eBook Packages: Computer ScienceComputer Science (R0)