Abstract
Despite the importance of Model Based System Engineering (MBSE) for early design verification, it is always challenging to represent the system properties / constraints at higher abstraction level due to complex behavioral and temporal aspects of embedded systems. To manage this, OCL (Object Constraint Language) and CCSL (Clock Constraint Specification Language) have been frequently used. On the other hand, SystemVerilog is a renowned hardware design and verification language that supports Assertion Based Verification (ABV). However, no real efforts have been made to employ SystemVerilog Assertions (SVA’s) in MBSE. In this paper, we explore various possibilities to represent SVA’s at higher abstraction level. Firstly, we evaluate the existing property specification approaches to represent SVA’s at higher abstraction level. Consequently, we select OCL as an appropriate approach. Secondly, we investigate the syntax and semantics of OCL in the context of SVA’s. The outcomes of research provide the sound platform to represent SVA’s in OCL for model-based design verification of embedded systems.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Rashid, M., Anwar, M.W., Khan, A.M.: Towards the Tools Selection in Model Based System Engineering for Embedded Systems - A Systematic Literature Review. JSS 106, 150–163 (2015)
Booch, G., Rumbaugh, J., Jacobson, I.: UML, User Guide. Addison-Wesley (1999)
OMG, SysML (2008). http://www.omg.org/spec/SysML/1.3/ (retrieved March 6, 2012)
OMG, UML Profile for MARTE, v1.0, November 2009, formal/2009-11-02
Knorreck, D., Apvrille, L.: TEPE: A SysML Language for Time-Constrained Property Modeling and Formal Verification. ACM SIGSOFT 36(1), 1–8 (2011)
Ge, N., Pantel, M., Cregut, X.: Formal specification and verification of task time constraints for real-time systems. LNCS, vol. 7610, pp. 143–157 (2012)
Baresi, L., Blohm, G., Kolovos, D.S., Matragkas, N., Motta, A., Paige, R.F., Radjenovic, A., Rossi, M.: Formal verification and validation of embedded systems: the UML-based MADES approach. SSM Springer (2013)
MODEVES project, details of SLR. http://www.modeves.com/slr2.html
Object management Group: http://www.omg.org/ (accessed September 2015)
Object Constraint Language: http://www.omg.org/spec/OCL/ (accessed September 2015)
Clock Constraint Specification Language (CCSL): http://www.omgmarte.org/node/66 (accessed September 2015)
Rashid, M., Anwar, M.W., Khan, A.M.: Identification of trends for model based development of embedded systems. In: 12th IEEE International Symposium on Programming and Systems (ISPS), April 2015, Algiers, pp. 1–8 (2015)
Rashid, M., Pottier, B.: A multi-objective framework for characterization of software specifications. In: Embedded and Real Time System Development: A Software Engineering Perspective: Concepts, Methods and Principles. Springer, pp. 185–209 (2014)
Rashid, M.: An efficient cycle accurate performance estimation model for hardware software co-design. In: Embedded and Real Time System Development: A Software Engineering Perspective: Concepts, Methods and Principles. Springer, pp. 213–234 (2014)
Rashid, M., Ferrandi, F., Bertels, K.: HARTES design flow for heterogeneous platforms. In: Proceedings of the 10th International Symposium on Quality of Electronic Design (ISQED 2009), CA, USA, March 2009, pp. 330–338 (2009)
IEEE SystemVerilog: http://standards.ieee.org/getieee/1800/download/1800-2012.pdf
Jin, N., Shen, C., Ni, T.: Engineering of An Assertion-based PSLSimple-Verilog Dynamic Verifier by Alternating Automata. ENTCS 207, 153–169 (2008)
Li, L., Coyle, F.P., Thornton, M.A.: UML to SystemVerilog synthesis for embedded system models with support for assertion generation. In: ECSI Forum on Design Languages (2007)
Andrade, E., Maciel, P., Callou, G., Nogueira, B.: A methodology for mapping SysML activity diagram to time petri net for requirement validation of embedded real-time systems with energy constraints. In: ICDS 2009, pp. 266–271 (2009)
Moreira, T.G., Wehrmeister, M., Pereira, C.E., Pétin, J.F., Levrat, E.: Automatic code generation for embedded systems: from UML specifications to VHDL code. In: IEEE 8th INDIN 2010, pp. 1085–1090 (2010)
Huang, X., Sun, Q., Li, J., Pan, M., Zhang, T.: An MDE-based approach to the verification of SysML state machine diagram. In: APSIS 2012, p. 9. ACM (2012)
Benveniste, A., Caspi, P., Edwards, S., Halbwachs, N., Le Guernic, P., De Simone, R.: The synchronous languages 12 years later. Proc. of the IEEE 91(1), 64–83
André, C., Mallet, F., Deantoni, J.: VHDL observers for clock constraint checking. In: ISIE, pp. 98–107
Peters, J., Wille, R., Drechsler, R.: Generating SystemC implementations for clock constraints specified in UML/MARTE CCSL. In: 19th ICECCS 2014, pp. 116–125 (2014)
Suryadevara, J.: Validating EAST-ADL timing constraints using UPPAAL. In: 39th Euromicro Conference SEAA 2013, pp. 268–275 (2013)
Berrani, S., Hammad, A., Mountassir, H.: Mapping SysML to modelica to validate wireless sensor networks non-functional requirements. In: 11th ISPS 2013, pp. 177–186 (2013)
Modelica Language: https://www.modelica.org/ (accessed October 2015)
Rahman, M.A.A., Nor, N.S.M., Mizukawa, M.: Evaluation for SysML-based design and analysis models using PCE. In: ICCSCE 2012, pp. 339–344 (2012)
Iqbal, M.Z., Arcuri, A., Briand, L.: Environment modeling and simulation for automated testing of soft real-time embedded software. SSM (2013)
Bousse, E., Mentré, D., Combemale, B., Baudry, B., Katsuragi, T.: Aligning SysML with the B method to provide V&V for systems engineering. In: WMDEVV, pp. 11–16. ACM (2012)
Universal Verification Methodology: http://accellera.org/downloads/standards/uvm
Bradfield, J., Filipe, J. K., Stevens, P.: Enriching OCL using observational mu-calculus. LNCS, vol. 2306, pp. 203–217 (2002)
Mullins, J., Oarga, R.: Model checking of extended OCL constraints on UML models in SOCLe. LNCS, vol. 4468, pp. 59–75 (2007)
Mentor Graphics: http://www.mentor.com/ (accessed October 2015)
Lavazza, Luigi, Morasca, Sandro, Morzenti, Angelo: A Dual Language Approach to the Development of Time-Critical Systems. ENTC 116, 227–239 (2005)
Cengarle, M.V., Knapp, A.: Towards OCL/RT. LNCS, vol. 2391, pp. 390–409
Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: 21st ICS, pp. 411–420 (1999)
Dou, W., Bianculli, D., Briand, L.: OCLR: a more expressive, pattern-based temporal extension of OCL. LNCS, vol. 8569, pp. 51–66 (2014)
Kanso, B., Taha, S.: Specification of temporal properties with OCL. Science of Computer programming 96, Part 4, pp. 527–551 (2014)
Ali, S., Iqbal, M.Z., Arcuri, A., Briand, L.: A Search-based OCL constraint solver for model-based test data generation. In: The 11th International Conference on Quality Software (2011)
Bill, R., Gabmeyer, S., Kaufmann, P., Seidl, M.: Model checking of CTL-extended OCL specifications. LNCS, vol. 8706, pp. 221–240 (2014)
Baier, C., Katoen, J.P.: Principles of model checking. The MIT Press (2008)
Emerson, E.: Temporal and modal logic. In: Leeuwen, J.V. (ed.) HTCE. MIT Press (1990)
IEEE PSL Std.: http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=5446004
Ouchani, S., Mohamed, O.A., Debbabi, M.: A formal verification framework for SysML activity diagrams. ESA, 2713–2728 (2014)
Siveroni, I., Zisman, A., Spanoudakis, G.: Property specification and static verification of UML models. In: 3rd ICARS 2008, pp. 96–103 (2008)
Di Guglielmo, G., Di Guglielmo, L., Foltinek, A., Fujita, M., Fummi, F., Marconcini, C., Pravadelli, G.: On the integration of model-driven design and dynamic assertion-based verification for embedded software. JSS, 2013–2033 (2013)
Rashid, M., Picard, D., Pottier, B.: Application analysis for parallel processing. In: Proceedings of the 11th Euro Micro Conference on Digital System Design, Architectures, Methods and Tools (DSD 2008), Parma, Italy, September 2008, pp. 633–640 (2008)
Eciplse XText Editor: https://eclipse.org/Xtext/ (accessed October 2015)
Papyrus MDT: http://www.eclipse.org/modeling/mdt/papyrus/
OMG, M2M/Operational QTV: https://projects.eclipse.org/projects/modeling.mmt.qvt-oml
Yin, L., Liu, J., Ding, Z., Mallet, F., De Simone, R.: Schedulability analysis with CCSL specifications. In: 20th APSEC 2013, pp. 414–421 (2013)
TimeSquare: http://timesquare.inria.fr/ (accessed August 2015)
IBM: Rational PCE. http://www.304.ibm.com/support/docview.wss?uid=swg27018723
MofScript: http://www.eclipse.org/gmt/mofscript/ (accessed August 2015)
Object Constraint Language specification version 2.4. http://www.omg.org/spec/OCL/2.4/
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer Science+Business Media Singapore
About this paper
Cite this paper
Rashid, M., Anwar, M.W., Azam, F., Kashif, M. (2016). Exploring the Platform for Expressing SystemVerilog Assertions in Model Based System Engineering. In: Kim, K., Joukov, N. (eds) Information Science and Applications (ICISA) 2016. Lecture Notes in Electrical Engineering, vol 376. Springer, Singapore. https://doi.org/10.1007/978-981-10-0557-2_53
Download citation
DOI: https://doi.org/10.1007/978-981-10-0557-2_53
Published:
Publisher Name: Springer, Singapore
Print ISBN: 978-981-10-0556-5
Online ISBN: 978-981-10-0557-2
eBook Packages: EngineeringEngineering (R0)