Top

Published in:

2021 | OriginalPaper | Chapter

Cross-level Co-simulation and Verification of an Automatic Transmission Control on Embedded Processor

Authors : Cinzia Bernardeschi, Andrea Domenici, Maurizio Palmieri, Sergio Saponara, Tanguy Sassolas, Arief Wicaksana, Lilia Zaourar

Published in: Software Engineering and Formal Methods. SEFM 2020 Collocated Workshops

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

This work proposes a method for the development of cyber-physical systems starting from a high-level representation of the control algorithm, performing a formal analysis of the algorithm, and co-simulating the algorithm with the controlled system both at high level, abstracting from the target processor, and at low level, i.e., including the emulation of the target processor. The expected advantages are a smoother and more controllable development process and greater design dependability and accuracy with respect to basic model-driven development. As a case study, an automatic transmission control has been used to show the applicability of the proposed approach.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Modelling Train Driver Behaviour in Railway Co-simulations

next chapter A Semantic-Aware, Accurate and Efficient API for (Co-)Simulation of CPS

Available only for authorised users

https://www.mathworks.com/help/simulink/slref/modeling-an-automatic-transmission-controller.html.

Accelera: TLM-2.0 Language Reference Manual (2009). https://www.accellera.org/images/downloads/standards/systemc/TLM_2_0_LRM.pdf

Bellard, F.: QEMU, a fast and portable dynamic translator. In: Proceedings of the Annual Conference on USENIX Annual Technical Conference, ATEC 2005, p. 41. USENIX Association, USA (2005)

Bernardeschi, C., Domenici, A., Masci, P.: A PVS-simulink integrated environment for model-based analysis of cyber-physical systems. IEEE Trans. Softw. Eng. 44(6), 512–533 (2018)CrossRef

Blochwitz, T., et al.: Functional mockup interface 2.0: the standard for tool independent exchange of simulation models. In: Proceedings of the 9th International MODELICA Conference, pp. 173–184. No. 76 in Linköping Electronic Conference Proceedings (2012)

Bohrer, B., Rahli, V., Vukotic, I., Völp, M., Platzer, A.: Formally verified differential dynamic logic. In: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, pp. 208–221. ACM (2017). https://doi.org/10.1145/3018610.3018616

Charif, A., Busnot, G., Mameesh, R.H., Sassolas, T., Ventroux, N.: Fast virtual prototyping for embedded computing systems design and exploration. In: Chillet, D. (ed.) Proceedings of the Rapid Simulation and Performance Evaluation: Methods and Tools, RAPIDO 2019, Valencia, Spain, 21–23 January 2019, pp. 3:1–3:8. ACM (2019). https://doi.org/10.1145/3300189.3300192

Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: HyComp: an SMT-based model checker for hybrid systems. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 52–67. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46681-0_4CrossRef

De Moura, L., Bjørner, N.: Satisfiability modulo theories: introduction and applications. Commun. ACM 54(9), 69–77 (2011)CrossRef

Domenici, A., Fagiolini, A., Palmieri, M.: Integrated simulation and formal verification of a simple autonomous vehicle. In: Cerone, A., Roveri, M. (eds.) SEFM 2017. LNCS, vol. 10729, pp. 300–314. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-74781-1_21CrossRef

10.

Franchetti, F., et al.: High-assurance spiral: end-to-end guarantees for robot and car control. IEEE Control Syst. 37(2), 82–103 (2017). https://doi.org/10.1109/MCS.2016.2643244MathSciNetCrossRef

11.

Gomes, C., Thule, C., Broman, D., Larsen, P.G., Vangheluwe, H.: Co-simulation: a survey. ACM Comput. Surv. (CSUR) 51(3), 1–33 (2018)CrossRef

12.

Henzinger, T.A.: The theory of hybrid automata. In: Inan, M.K., Kurshan, R.P. (eds.) Verification of Digital and Hybrid Systems. NATO ASI Series (Series F: Computer and Systems Sciences), vol. 170, pp. 265–292. Springer, Heidelberg (2000). https://doi.org/10.1007/978-3-642-59615-5_13CrossRef

13.

IEEE: IEEE Standard for Standard SystemC Language Reference Manual. IEEE Std 1666–2011 (Revision of IEEE Std 1666–2005), pp. 1–638 (2012)

14.

Imperas Ltd.: Open Virtual Platforms (2020). http://www.ovpworld.org/

15.

Larsen, P.G., et al.: Integrated tool chain for model-based design of Cyber-Physical Systems: the INTO-CPS project. In: 2016 2nd International Workshop on Modelling, Analysis, and Control of Complex CPS (CPS Data), pp. 1–6, April 2016. https://doi.org/10.1109/CPSData.2016.7496424

16.

Masci, P., et al.: Combining PVSio with Stateflow. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2014. LNCS, vol. 8430, pp. 209–214. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-06200-6_16CrossRef

17.

Mauro, G., Thimbleby, H., Domenici, A., Bernardeschi, C.: Extending a user interface prototyping tool with automatic MISRA C code generation. In: Dubois, C., Masci, P., Méry, D. (eds.) Third Workshop on Formal Integrated Development Environments. Electronic Proceedings in Theoretical Computer Science, vol. 240, pp. 53–66. Open Publishing Association (2017). https://doi.org/10.4204/EPTCS.240.4

18.

Oladimeji, P., Masci, P., Curzon, P., Thimbleby, H.: PVSio-web: a tool for rapid prototyping device user interfaces in PVS. In: FMIS 2013, 5th International Workshop on Formal Methods for Interactive Systems, London, UK, 24 June 2013 (2013)

19.

Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748–752. Springer, Heidelberg (1992). https://doi.org/10.1007/3-540-55602-8_217CrossRef

20.

Palmieri, M., Bernardeschi, C., Masci, P.: A framework for FMI-based co-simulation of human-machine interfaces. Softw. Syst. Model. 19(3), 601–623 (2020)CrossRef

21.

Palmieri, M., Macedo, H.D.: Automatic generation of functional mock-up units from formal specifications. In: Camara, J., Steffen, M. (eds.) SEFM 2019. LNCS, vol. 12226, pp. 27–33. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-57506-9_3CrossRef

22.

Platzer, A., Quesel, J.-D.: KeYmaera: a hybrid theorem prover for hybrid systems (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 171–178. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-71070-7_15CrossRef

23.

Püschel, M., et al.: SPIRAL: code generation for DSP transforms. Proc. IEEE 93(2), 232–275 (2005). https://doi.org/10.1109/JPROC.2004.840306CrossRef

24.

Saidi, S.E., Charif, A., Sassolas, T., Le Guay, P.G., Souza, H.V., Ventroux, N.: Fast virtual prototyping of cyber-physical systems using SystemC and FMI: ADAS use case. In: Proceedings of the 30th International Workshop on Rapid System Prototyping (RSP 2019), pp. 43–49 (2019)

25.

Selic, B.: The pragmatics of model-driven development. IEEE Softw. 20(5), 19–25 (2003). https://doi.org/10.1109/MS.2003.1231146CrossRef

26.

Synopsys: Virtualizer (2020). https://www.synopsys.com/verification/virtual-prototyping/virtualizer.html

27.

Ventroux, N., et al.: SESAM: an MPSoC simulation environment for dynamic application processing. In: 2010 10th IEEE International Conference on Computer and Information Technology, pp. 1880–1886 (2010). https://doi.org/10.1109/CIT.2010.322

Title: Cross-level Co-simulation and Verification of an Automatic Transmission Control on Embedded Processor
Authors: Cinzia Bernardeschi
Andrea Domenici
Maurizio Palmieri
Sergio Saponara
Tanguy Sassolas
Arief Wicaksana
Lilia Zaourar
Publisher: Springer International Publishing
Book: Software Engineering and Formal Methods. SEFM 2020 Collocated Workshops
Print ISBN: 978-3-030-67219-5

Electronic ISBN: 978-3-030-67220-1

Copyright Year: 2021
DOI: https://doi.org/10.1007/978-3-030-67220-1_20

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner