Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Genericity in PAR Platform Read chapter Read first chapter

2016 | OriginalPaper | Chapter

Model Checking Process Scheduling over Multi-core Computer System with MSVL

Authors : Xinfeng Shu, Zhenhua Duan

Published in: Structured Object-Oriented Formal Language and Method

Publisher: Springer International Publishing

Log in

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

search-config
loading …

Abstract

To solve the problem that software testing cannot meet the verification needs of process scheduling over multi-core computer system, a model checking approach with MSVL is adapted to verify the correctness of process scheduling. Firstly, the grammar of MSVL is briefly introduced; further, a general model supporting the most commonly used scheduling algorithms for multi-core computer is formalized by MSVL program; finally, as a case study, the safeness of the processes scheduler with the earliest deadline first(EDF) scheduling algorithm over a 2-core CPU is verified with MSV toolkit, which indicates the proposed approach can effectively solve the verification problems of process scheduling over multi-core CPU.

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 Automated Program Debugging for Multiple Bugs Based on Semantic Analysis
next chapter A Method Based on MSVL for Verification of the Social Network Privacy Policy
Literature
1.
Wijs, A., van de Pol, J., Bortnik, E.M.: Solving scheduling problems by untimed model checking. STTT 11(5), 375–392 (2009)CrossRef
2.
Ruys, T.C.: Optimal scheduling using branch and bound with SPIN 4.0. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 1–17. Springer, Heidelberg (2003)CrossRef
3.
Lime, D., Roux, O.H.: Formal verification of real-time systems with preemptive scheduling. Real-Time Syst. 41(2), 118–151 (2009)CrossRefMATH
4.
Duan, Z.: An extended interval temporal logic and a framing technique for interval temporal logic programming. Ph.D. thesis, University of Newcastle Upon Tyne, May 1996
5.
Duan, Z.: Temporal Logic and Temporal Logic Programming. Science Press, Beijing (2005)
6.
Duan, Z., Tian, C., Zhang, L.: A decision procedure for propositional projection temporal logic with infinite models. Acta Inf. 45(1), 43–78 (2008)MathSciNetCrossRefMATH
7.
Tian, C., Duan, Z.: Expressiveness of propositional projection temporal logic with star. Theor. Comput. Sci. 412(18), 1729–1744 (2011)MathSciNetCrossRefMATH
8.
Duan, Z., Koutny, M.: A Framed Temporal Logic Programming Language. J. Comput. Sci. Technol. 19, 333–344 (2004)MathSciNet
9.
10.
Duan, Z., Tian, C.: A unified model checking approach with projection temporal logic. In: Liu, S., Araki, K. (eds.) ICFEM 2008. LNCS, vol. 5256, pp. 167–186. Springer, Heidelberg (2008)CrossRef
11.
Wang, M., Duan, Z., Tian, C.: Simulation and verification of the virtual memory management system with MSVL. In: Proceedings of the 2014 IEEE 18th International Conference on Computer Supported Cooperative Work in Design (CSCWD), pp. 360–365, May 2014
12.
Cui, J., Duan, Z., Tian, C., Zhang, N., Zhou, C.: Model Checking \(\mu \) C/OS-III Multi-task System with TMSVL. In: Butler, M., Conchon, S., Zaïdi, F. (eds.) Formal Methods and Software Engineering. Lecture Notes in Computer Science, vol. 9407, pp. 187–200. Springer, Switzerland (2015)CrossRef
13.
Yu, Y., Duan, Z., Tian, C., Yang, M.: Model checking C programs with MSVL. In: Liu, S. (ed.) SOFL 2012. LNCS, vol. 7787, pp. 87–103. Springer, Heidelberg (2013)CrossRef
14.
Bin, Y., Duan, Z., Tian, C.: Bounded model checking of traffic light control system. Electr. Notes Theor. Comput. Sci. 309, 63–74 (2014)CrossRef
15.
Ma, Q., Duan, Z., Zhang, N., Wang, X.: Verification of distributed systems with the axiomatic system of MSVL. Formal Asp. Comput. 27(1), 103–131 (2015)MathSciNetCrossRefMATH
Metadata
Title
Model Checking Process Scheduling over Multi-core Computer System with MSVL
Authors
Xinfeng Shu
Zhenhua Duan
Copyright Year
2016
Publisher
Springer International Publishing
Book
Structured Object-Oriented Formal Language and Method

Print ISBN: 978-3-319-31219-4

Electronic ISBN: 978-3-319-31220-0

Copyright Year: 2016

DOI
https://doi.org/10.1007/978-3-319-31220-0_8

Premium Partner

    Image Credits