Scenario-based verification in presence of variability using a synchronous approach

Abstract

This paper presents a new model of scenarios, dedicated to the specification and verification of system behaviours in the context of software product lines (SPL). We draw our inspiration from some techniques that are mostly used in the hardware community, and we show how they could be applied to the verification of software components. We point out the benefits of synchronous languages and models to bridge the gap between both worlds.

Keywords

Esterel / UML MARTE / scenario / verification / feature interaction / variability

References

[1] Linden V d F, Schmid K, Rommes E. Software product lines in action. Springer-Verlag, 2007

[2] Classen A. Problem-oriented feature interaction detection in software product lines. In: Proceedings of the International Conference on Feature Interactions in Software and Communication Systems (ICFI). 2007

[3] Filho R S S, Redmiles D FManaging feature interaction by documenting and enforcing dependencies in software product lines. In: Proceedings of the International Conference on Feature Interactions in Software and Communication Systems (ICFI). 2007, 33−48

[4] Benveniste A, Caspi P, Edwards S A, Halbwachs N, Le Guernic P, Simone d R. The synchronous languages 12 years later. Proceedings of the IEEE, 2003, 91(1): 64−83

[5] The Esterel Team. Esterel Compiler 5.92.

[6] Reniers M A. Message sequence chart: syntax and semantics. PhD thesis, Eindhoven University of Technology, 1999

[7] . Object Management Group. OMG unified modeling language (OMG UML), Superstructure, V2.1.2. 2007

[8] Damm W, Harel D. LSCs: breathing life into message sequence charts. Formal Methods in System Design, 2001, 19: 45−80

[9] Wagner S, Cengarle M V, Graubmann P. Modelling system families with message sequence charts: a case study. Technical Report TUMI0416, Technische Universität München, 2004

[10] Ziadi T, Helouët L, Jézéquel J M. . Towards a UML profile for software product lines. In: Proceedings of the International Workshop on Product Family Engineering (PFE-5). 2003

[11] André C, Mallet F, Simone d R. Modeling time(s). Model Driven Engineering Languages and Systems. 2007, 559−573

[12] O’Leary J, Zhao X, Gerth R, Seger C J H. Formally verifying ieee compliance of floating-point hardware. Intel Technology Journal, 1999, Q1’99: 1−14

[13] Ramesh S, Bhaduri P. Validation of pipelined processor designs using Esterel tools: a case study. In: Proceedings of the International Conference on Computer Aided Verification (CAV’99). 1999, 84−95

[14] Bonifácio R, Borba P. Modeling scenario variability as crosscutting mechanisms. In: Proceedings of the International Conference on Aspect-oriented software development (AOSD’09). 2009, 125−136

[15] Cordy M, Schobbens P Y, Heymans P, Legay A. Beyond Boolean product-line model checking: dealing with feature attributes and multifeatures. In: Proceedings of the ACM/IEEE International Conference on Software Engineering (ICSE). 2013

[16] Millo J V, Ramesh S, Sankaranarayanan K, Narwane G K. Compositional verification of software product line. In: Proceedings of the International Conference on Integrated Formal Method, iFM. 2013

[17] Gruler A, Leucker M, Scheidemann K D. Modeling and model checking software product lines. In: Proceedings of the FMOODS. 2008: 113−131

[18] Liu J, Basu S, Lutz R. Compositional model checking of software product lines using variation point obligations. Automated Software Engineering, 2011, 18: 39−76.

[19] Lauenroth K, Pohl K, Toehning S. . Model checking of domain artifacts in product line engineering. In: Proceedings of the IEEE/ACM International Conference on Automated Software Engineering, ASE. 2009, 269−280

[20] Greenyer J, Sharifloo A M, Cordy M, Heymans P. Efficient consistency checking of scenario-based product-line specifications. In: Proceedings of the International Conference on Requirement Engineering (RE). 2012

[21] André C. SyncCharts: a visual representation of reactive behaviors. Technical Report RR96−56, I3S, Sophia-Antipolis, France, 1996

[22] André C. Synchronous interface behavior: syntax and semantics. Technical Report RR00−11, I3S, Sophia-Antipolis, France, 2000

[23] André C, Péraldi M A, Rigault J P. Scenario and property checking of real-time systems using a synchronous approach. In: Proceedings of ISORC. 2001, 438−444

[24] Benveniste A, Berry G. The synchronous approach to reactive and realtime systems. Proceedings of the IEEE, 1991, 79(9): 1270−1282

[25] Halbwachs N. Synchronous programming of reactive systems. Kluwer Academic Pub., 1993

[26] Schneider K. The synchronous programming language quartz. Technical report, Department of Computer Science, University of Kaiserslautern, 2009

[27] Traulsen C, Amende T, Hanxleden v R. Compiling synccharts to synchronous c. In: Design, Automation Test in Europe Conference Exhibition (DATE’11). 2011, 1−4

[28] Potop-Butucaru D, Edwards S, Berry G. Compiling Esterel. GeoJournal library. Springer, 2007

[29] Pohl K, Buckle G, Linden v. d F. . Software product line engineering: foundations, principles, and techniques. Springer, Berlin Heidelberg New York, 2005. ISBN: 3-540-24372-0

[30] Krueger C W. . New methods in software product line practice. Communications of ACM, 2006, 49(12): 37−40

[31] Flores R, Krueger C, Clements P. Mega-scale product line engineering at general motors. In: Proceedings of SPLC. 2012, 259−269

[32] OMG. UML Profile for MARTE, v1.0. Object management group, 2009. formal/2009-11-02

[33] André C. Syntax and semantics of the clock constraint specification language (CCSL). Research Report 6925, INRIA, 2009

[34] Le Guernic P, Talpin J P, Le Lann J C. Polychrony for system design. Journal of Circuits, Systems, and Computers, 2003, 12(3): 261−304

[35] Lee E A, . Sangiovanni-Vincentelli A L. A framework for comparing models of computation. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1998, 17(12): 1217−1229

[36] André C, Mallet F. Specification and verification of time requirements with CCSL and esterel. In: Proceedings of LCTES. 2009, 167−176

[37] Boucaron J, Gaffé D. SyncCharts compiler collection.

[38] Tripakis S, Sofronis C, Caspi P, Curic A. Translating discrete-time simulink to lustre. ACM Transactions on Embedded Computing Systems, 2005

[39] Beeck V. d M. A comparison of Statecharts variants. In: Proceedings of the International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems. 1994, 128−148

[40] Harel D, Kugler H. The Rhapsody semantics of Statecharts. In: LNCS. 2004, 325−354

[41] Prochnow S, Traulsen C, Hanxleden v R. Synthesizing safe state machines from Esterel. In: Proceedings of the International Conference on Language, Compilers, and Tool Support for Embedded Systems (LCTES’06), 2006, 41: 113−124

[42] Batory D. Feature models, grammars, and propositional formulas. In: Software Product Lines, Volume 3714 of LNCS, 7−20. Springer Berlin /Heidelberg, 2005

[43] Bouali A. Xeve: an Esterel verification environment (version v1_3). Technical Report RT-0214, INRIA, Sophia-Antipolis, 1997

[44] Emerson E A. Temporal and modal logic. In: Handbook Of Theoretical Computer Science. 1995, 995−1072

[45] Berkeley Logic Synthesis and Verification Group. ABC, release 10216. http://www.eecs.berkeley.edu/ãlanmi/abc/

[46] Aho A V, Corasick M JEfficient string matching: An aid to bibliographic search. Communications of the ACM, 1975, 18: 333−340

RIGHTS & PERMISSIONS

2013 Higher Education Press and Springer-Verlag Berlin Heidelberg