More Web Proxy on the site http://driver.im/

research-article

Qualitative and quantitative analysis with scheduling policies in model checking

Authors:

Toshiaki AokiAuthors Info & Claims

SAC '18: Proceedings of the 33rd Annual ACM Symposium on Applied Computing

Pages 1873 - 1880

https://doi.org/10.1145/3167132.3167332

Published: 09 April 2018 Publication History

Abstract

An execution order of the processes in a system depends on the scheduler. Therefore, the scheduling strategy needs to be taken into account during the analysis of the system behaviors. The goal of this research is to improve the support for analyzing concurrent systems executed under different scheduling policies. A domain-specific language (DSL) is proposed to provide an effective specification of various schedulers. Necessary artifacts for the analysis are generated automatically. Based on the specification of the scheduler, an algorithm to explore the state space is realized. We use discrete time to consider a transition from a state to another state taking one time unit during the search. A graph is determined from the state space. To analyze the behaviors of the system, this graph is then labeled following an input formula which represents a qualitative/quantitative property. The results of applying our approach to several scheduling policies demonstrated that the system with scheduling policies could be analyzed accurately and easily.

References

[1]

SSpinJa. http://jaist.ac.jp/~s1520209/sspinja.html, Accessed: 20-April-2017.

[2]

T. Amnell, E. Fersman, L. Mokmshin, P. Pettersson, and W. Yi. TIMES: a tool for schedulability analysis and code generation of real-time systems. In International Conference on Formal Modeling and Analysis of Timed Systems, pages 60--72. Springer, 2003.

[3]

T. Aoki. Model checking multi-task software on real-time operating systems. In 2008 11th IEEE International Symposium on Object and Component-Oriented Real-Time Distributed Computing (ISORC), pages 551--555. IEEE, 2008.

Digital Library

[4]

L. Bettini. Implementing domain-specific languages with Xtext and Xtend. Packt Publishing Ltd, 2016.

Digital Library

[5]

A. M. Cheng. Real-time systems: scheduling, analysis, and verification. John Wiley & Sons, 2003.

Digital Library

[6]

E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems (TOPLAS), 8(2):244--263, 1986.

Digital Library

[7]

A. David, J. Illum, K. G. Larsen, and A. Skou. Model-based framework for schedulability analysis using UPPAAL 4.1. Model-based design for embedded systems, 1(1):93--119, 2009.

[8]

M. de Jonge and T. C. Ruys. The SpinJa model checker. In International SPIN Workshop on Model Checking of Software, pages 124--128. Springer, 2010.

Digital Library

[9]

S. Di Alesio, S. Nejati, L. Briand, and A. Gotlieb. Stress testing of task deadlines: A constraint programming approach. In 2013 IEEE 24th International Symposium on Software Reliability Engineering (ISSRE), pages 158--167. IEEE, 2013.

[10]

B. Dushnik and E. W. Miller. Partially ordered sets. American journal of mathematics, 63(3):600--610, 1941.

[11]

E. A. Emerson, A. K. Mok, A. P. Sistla, and J. Srinivasan. Quantitative temporal reasoning. Real-Time Systems, 4(4):331--352, 1992.

Digital Library

[12]

R. Gerth. Concise PROMELA reference, 1997. http://spinroot.com/spin/Man/Quick.html, Accessed: April 20, 2017.

[13]

H. Gomaa. Designing concurrent, distributed, and real-time applications with UML. In Proceedings of the 23rd international conference on software engineering, pages 737--738. IEEE Computer Society, 2001.

Digital Library

[14]

G. Holzmann. Spin model checker, the: primer and reference manual. Addison-Wesley Professional, 2003.

Digital Library

[15]

K. G. Larsen, P. Pettersson, and W. Yi. UPPAAL in a nutshell. International Journal on Software Tools for Technology Transfer (STTT), 1(1):134--152, 1997.

Digital Library

[16]

J. P. Lehoczky and S. Ramos-Thuel. An optimal algorithm for scheduling soft-aperiodic tasks in fixed-priority preemptive systems. In Real-Time Systems Symposium, 1992, pages 110--123. IEEE, 1992.

[17]

U. MARTE. UML profile for MARTE: modeling and analysis of real-time embedded systems, 2015.

[18]

T. Nhat-Hoa, Y. Chiba, and T. Aoki. Domain-specific language facilitates scheduling in model checking. In 24th Asia-Pacific Software Engineering Conference (APSEC), pages 417--426. IEEE, 2017.

[19]

R. Pelánek. Beem: Benchmarks for explicit model checkers. In International SPIN Workshop on Model Checking of Software, pages 263--267. Springer, 2007.

Digital Library

[20]

K. Tindell and J. Clark. Holistic schedulability analysis for distributed hard real-time systems. Microprocessing and microprogramming, 40(2-3):117--134, 1994.

Digital Library

Cited By

Nhat-Hoa TAoki T(2021)SSpinJa: Facilitating Schedulers in Model Checking2021 IEEE 21st International Conference on Software Quality, Reliability and Security (QRS)10.1109/QRS54544.2021.00073(632-641)Online publication date: Dec-2021
https://doi.org/10.1109/QRS54544.2021.00073

Index Terms

Qualitative and quantitative analysis with scheduling policies in model checking
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Formal software verification

Recommendations

Global EDF-based scheduling with laxity-driven priority promotion

This paper presents an algorithm, called Earliest Deadline Critical Laxity (EDCL), for scheduling sporadic task systems on multiprocessors. EDCL is a derivative of the Earliest Deadline Zero Laxity (EDZL) algorithm. Each job is assigned a priority based ...
Preemptive Hadoop Jobs Scheduling under a Deadline
SKG '12: Proceedings of the 2012 Eighth International Conference on Semantics, Knowledge and Grids

MapReduce has become the dominant programming model in a cloud-based data processing environment, such as Hadoop. First In First Out (FIFO) is the default job scheduling policy of Hadoop, but it cannot guarantee that the job will be completed by a ...
EDZL Schedulability Analysis in Real-Time Multicore Scheduling

In real-time systems, correctness depends not only on functionality but also on timeliness. A great number of scheduling theories have been developed for verification of the temporal correctness of jobs (software) in such systems. Among them, the ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

SAC '18: Proceedings of the 33rd Annual ACM Symposium on Applied Computing

April 2018

2327 pages

ISBN:9781450351911

DOI:10.1145/3167132

Conference Chairs:
Hisham M. Haddad
Kennesaw State University
,
Roger L. Wainwright
University of Tulsa
,
Richard Chbeir
University of Pau & Pays Adour, France

Copyright © 2018 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGAPP: ACM Special Interest Group on Applied Computing

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 09 April 2018

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

SAC 2018

Sponsor:

SIGAPP

SAC 2018: Symposium on Applied Computing

April 9 - 13, 2018

Pau, France

Acceptance Rates

Overall Acceptance Rate 1,650 of 6,669 submissions, 25%

Upcoming Conference

SAC '25

Sponsor:
sigapp

The 40th ACM/SIGAPP Symposium on Applied Computing

March 31 - April 4, 2025

Catania , Italy

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

1
Total Citations
View Citations
86
Total Downloads

Downloads (Last 12 months)5
Downloads (Last 6 weeks)0

Reflects downloads up to 13 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Nhat-Hoa TAoki T(2021)SSpinJa: Facilitating Schedulers in Model Checking2021 IEEE 21st International Conference on Software Quality, Reliability and Security (QRS)10.1109/QRS54544.2021.00073(632-641)Online publication date: Dec-2021
https://doi.org/10.1109/QRS54544.2021.00073

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents