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

doi:10.1007/s11704-013-3094-6

Front. Comput. Sci.

2013, Vol. 7

Issue (5) : 650-672 https://doi.org/10.1007/s11704-013-3094-6

RESEARCH ARTICLE

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

Jean-Vivien MILLO¹(

), Frédéric MALLET², Anthony COADOU³, S RAMESH³

¹. INRIA Sophia-Antipolis, Aoste team (INRIA/I3S/CNRS/UNS), Sophia-Antipolis 06560, France
². University of Nice Sophia Antipolis, Sophia-Antipolis 06900, France
³. Global General Motors R&D, India Science Lab, GM Technical Center India, Bangalore 560066, India

Download: PDF(0 KB)
Export: BibTeX | EndNote | Reference Manager | ProCite | RefWorks

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

Corresponding Author(s): Jean-Vivien MILLO

Issue Date: 01 October 2013

Cite this article:

Jean-Vivien MILLO,Frédéric MALLET,Anthony COADOU, et al. Scenario-based verification in presence of variability using a synchronous approach[J]. Front. Comput. Sci., 2013, 7(5): 650-672.

URL:

https://academic.hep.com.cn/fcs/EN/10.1007/s11704-013-3094-6
https://academic.hep.com.cn/fcs/EN/Y2013/V7/I5/650

1	V d F Linden , K Schmid , E Rommes . Software product lines in action. Springer-Verlag, 2007
2	A Classen . 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	R S S Filho , D F Redmiles Managing 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	A Benveniste , P Caspi , S A Edwards , N Halbwachs , P Le Guernic , d R Simone . The synchronous languages 12 years later. Proceedings of the IEEE, 2003, 91(1): 64−83 https://doi.org/10.1109/JPROC.2002.805826
5	The Esterel Team. Esterel Compiler 5.92.
6	M A Reniers . 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	W Damm , D Harel . LSCs: breathing life into message sequence charts. Formal Methods in System Design, 2001, 19: 45−80 https://doi.org/10.1023/A:1011227529550
9	S Wagner , M V Cengarle , P Graubmann . Modelling system families with message sequence charts: a case study. Technical Report TUMI0416, Technische Universität München, 2004
10	T Ziadi , L Helouët , J M Jézéquel . . Towards a UML profile for software product lines. In: Proceedings of the International Workshop on Product Family Engineering (PFE-5). 2003
11	C André , F Mallet , R Simone d . Modeling time(s). Model Driven Engineering Languages and Systems. 2007, 559−573
12	J O’Leary , X Zhao , R Gerth , C J H Seger . Formally verifying ieee compliance of floating-point hardware. Intel Technology Journal, 1999, Q1’99: 1−14
13	S Ramesh , P Bhaduri . 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 https://doi.org/10.1007/3-540-48683-6_10
14	R Bonifácio , P Borba . Modeling scenario variability as crosscutting mechanisms. In: Proceedings of the International Conference on Aspect-oriented software development (AOSD’09). 2009, 125−136
15	M Cordy , P Y Schobbens , P Heymans , A Legay . 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	J V Millo , S Ramesh , K Sankaranarayanan , G K Narwane . Compositional verification of software product line. In: Proceedings of the International Conference on Integrated Formal Method, iFM. 2013
17	A Gruler , M Leucker , K D Scheidemann . Modeling and model checking software product lines. In: Proceedings of the FMOODS. 2008: 113−131
18	J Liu , S Basu , R Lutz . Compositional model checking of software product lines using variation point obligations. Automated Software Engineering, 2011, 18: 39−76. https://doi.org/10.1007/s10515-010-0075-7
19	K Lauenroth , K Pohl , S Toehning . . 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	J Greenyer , A M Sharifloo , M Cordy , P Heymans . Efficient consistency checking of scenario-based product-line specifications. In: Proceedings of the International Conference on Requirement Engineering (RE). 2012
21	C André . SyncCharts: a visual representation of reactive behaviors. Technical Report RR96−56, I3S, Sophia-Antipolis, France, 1996
22	C André . Synchronous interface behavior: syntax and semantics. Technical Report RR00−11, I3S, Sophia-Antipolis, France, 2000
23	C André , M A Péraldi , J P Rigault . Scenario and property checking of real-time systems using a synchronous approach. In: Proceedings of ISORC. 2001, 438−444
24	A Benveniste , G Berry . The synchronous approach to reactive and realtime systems. Proceedings of the IEEE, 1991, 79(9): 1270−1282 https://doi.org/10.1109/5.97297
25	N Halbwachs . Synchronous programming of reactive systems. Kluwer Academic Pub., 1993 https://doi.org/10.1007/978-1-4757-2231-4
26	K Schneider . The synchronous programming language quartz. Technical report, Department of Computer Science, University of Kaiserslautern, 2009
27	C Traulsen , T Amende , v R Hanxleden . Compiling synccharts to synchronous c. In: Design, Automation Test in Europe Conference Exhibition (DATE’11). 2011, 1−4
28	D Potop-Butucaru , S Edwards , G Berry . Compiling Esterel. GeoJournal library. Springer, 2007
29	K Pohl , G Buckle , v. d F Linden . . Software product line engineering: foundations, principles, and techniques. Springer, Berlin Heidelberg New York, 2005. ISBN: 3-540-24372-0
30	C W Krueger . . New methods in software product line practice. Communications of ACM, 2006, 49(12): 37−40 https://doi.org/10.1145/1183236.1183262
31	R Flores , C Krueger , P Clements . Mega-scale product line engineering at general motors. In: Proceedings of SPLC. 2012, 259−269 https://doi.org/10.1145/2362536.2362571
32	OMG. UML Profile for MARTE, v1.0. Object management group, 2009. formal/2009-11-02
33	C André . Syntax and semantics of the clock constraint specification language (CCSL). Research Report 6925, INRIA, 2009
34	P Le Guernic , J P Talpin , J C Le Lann . Polychrony for system design. Journal of Circuits, Systems, and Computers, 2003, 12(3): 261−304 https://doi.org/10.1142/S0218126603000763
35	E A Lee , . 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 https://doi.org/10.1109/43.736561
36	C André , F Mallet . Specification and verification of time requirements with CCSL and esterel. In: Proceedings of LCTES. 2009, 167−176 https://doi.org/10.1145/1542452.1542475
37	J Boucaron , D Gaffé . SyncCharts compiler collection.
38	S Tripakis , C Sofronis , P Caspi , A Curic . Translating discrete-time simulink to lustre. ACM Transactions on Embedded Computing Systems, 2005 https://doi.org/10.1145/1113830.1113834
39	V. d M Beeck . A comparison of Statecharts variants. In: Proceedings of the International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems. 1994, 128−148 https://doi.org/10.1007/3-540-58468-4_163
40	D Harel , H Kugler . The Rhapsody semantics of Statecharts. In: LNCS. 2004, 325−354
41	S Prochnow , C Traulsen , v R Hanxleden . 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	D Batory . Feature models, grammars, and propositional formulas. In: Software Product Lines, Volume 3714 of LNCS, 7−20. Springer Berlin /Heidelberg, 2005
43	A Bouali . Xeve: an Esterel verification environment (version v1_3). Technical Report RT-0214, INRIA, Sophia-Antipolis, 1997
44	E A Emerson . Temporal and modal logic. In: Handbook Of Theoretical Computer Science. 1995, 995−1072
45	Berkeley Logic Synthesis and Verification Group. ABC, release 10216.
46	A V Aho , M J Corasick Efficient string matching: An aid to bibliographic search. Communications of the ACM, 1975, 18: 333−340 https://doi.org/10.1145/360825.360855

[1]	Shahbaz ALI, Hailong SUN, Yongwang ZHAO. Model learning: a survey of foundations, tools and applications[J]. Front. Comput. Sci., 2021, 15(5): 155210-.
[2]	Daian YUE, Vania JOLOBOFF, Frédéric MALLET. TRAP: trace runtime analysis of properties[J]. Front. Comput. Sci., 2020, 14(3): 143201-.
[3]	Yuanrui ZHANG, Frédéric MALLET, Yixiang CHEN. A verification framework for spatio-temporal consistency language with CCSL as a specification language[J]. Front. Comput. Sci., 2020, 14(1): 105-129.
[4]	Tun LI, Jun YE, Qingping TAN. Towards functional verifying a family of SystemC TLMs[J]. Front. Comput. Sci., 2020, 14(1): 53-66.
[5]	Abdelkrim CHEBIEB, Yamine AIT AMEUR. A formal model for plastic human computer interfaces[J]. Front. Comput. Sci., 2018, 12(2): 351-375.
[6]	Yongwang ZHAO, Zhibin YANG, Dianfu MA. A survey on formal specification and verification of separation kernels[J]. Front. Comput. Sci., 2017, 11(4): 585-607.
[7]	Sedigheh KHOSHNEVIS, Fereidoon SHAMS. Automating identification of services and their variability for product lines using NSGA-II[J]. Front. Comput. Sci., 2017, 11(3): 444-464.
[8]	Ruifeng XU,Lin GUI,Qin LU,Shuai WANG,Jian XU. Incorporating multi-kernel function and Internet verification for Chinese person name disambiguation[J]. Front. Comput. Sci., 2016, 10(6): 1026-1038.
[9]	Jiankun HE,Xishun ZHAO. Reasoning about actions with loops via Hoare logic[J]. Front. Comput. Sci., 2016, 10(5): 870-888.
[10]	Xuzhou LI,Yilong YIN,Yanbin NING,Gongping YANG,Lei PAN. A hybrid biometric identification framework for high security applications[J]. Front. Comput. Sci., 2015, 9(3): 392-401.
[11]	Yu ZHOU,Yankai HUANG,Ou WEI,Zhiqiu HUANG. Verifying specifications with associated attributes in graph transformation systems[J]. Front. Comput. Sci., 2015, 9(3): 364-374.
[12]	Fei HE,Xiaoyu SONG,Ming GU,Jiaguang SUN. Generalized interface automata with multicast synchronization[J]. Front. Comput. Sci., 2015, 9(1): 1-14.
[13]	Xiaoxiao YANG,Yu ZHANG,Ming FU,Xinyu FENG. A temporal programming model with atomic blocks based on projection temporal logic[J]. Front. Comput. Sci., 2014, 8(6): 958-976.
[14]	Yuanjie SI, Jun SUN, Yang LIU, Jin Song DONG, Jun PANG, Shao Jie ZHANG, Xiaohu YANG. Model checking with fairness assumptions using PAT[J]. Front. Comput. Sci., 2014, 8(1): 1-16.
[15]	Van Chan NGO, Jean-Pierre TALPIN, Thierry GAUTIER, Paul Le GUERNIC, Loïc BESNARD. Formal verification of synchronous data-flow program transformations toward certified compilers[J]. Front. Comput. Sci., 2013, 7(5): 598-616.

Viewed

Full text

Abstract

Cited

Shared

Discussed