Back to first pageBack to first page Centre for Artificial Intelligence of UNL
Browse our site
You are here:

Publication details

Go back
Publication details
Main information
Modeling Assembly Program with Constraints: A Contribution to WCET Problem
September 2012
[Kafl12]
Model checking with program slicing has been successfully applied to compute Worst Case Execution Time(WCET) of a program running in a given hardware. This method lacks path feasibility analysis and suffers from additional problems. This thesis complements the above method with adopting constraint solving techniques to path feasibility analysis by a) validating the witness trace returned by the Model Checker and generate test data if it is executable; b) computing approximate WCET solely based on the program, suggesting probable paths that upper bound the WCET. This combination of constraint solving technique with model checking takes advantages of their strengths and makes WCET computation scalable and amenable to hardware changes. The techniques developed were tested on standard benchmark programs from Mälardalen University and compared with results obtained from model checking methods.
M. Sc. dissertation
Bishoksan Kafle
Pedro Barahona
Universidade Nova de Lisboa
-
-
Export formats
Bishoksan Kafle, Modeling Assembly Program with Constraints: A Contribution to WCET Problem, Pedro Barahona (superv.), Universidade Nova de Lisboa, September 2012.
<b>Bishoksan Kafle</b>, <u>Modeling Assembly Program with Constraints: A Contribution to WCET Problem</u>, <a href="/people/members/view.php?code=7e27bc13fad97e99cd21ea6914d55659" class="supervisor">Pedro Barahona</a> (superv.), Universidade Nova de Lisboa, September 2012.
@mastersthesis {[Kafl12], author = {Bishoksan Kafle}, title = {Modeling Assembly Program with Constraints: A Contribution to WCET Problem}, school = {Universidade Nova de Lisboa}, note = {Pedro Barahona (superv.); }, abstract = {Model checking with program slicing has been successfully applied to compute Worst Case Execution Time(WCET) of a program running in a given hardware. This method lacks path feasibility analysis and suffers from additional problems. This thesis complements the above method with adopting constraint solving techniques to path feasibility analysis by a) validating the witness trace returned by the Model Checker and generate test data if it is executable; b) computing approximate WCET solely based on the program, suggesting probable paths that upper bound the WCET. This combination of constraint solving technique with model checking takes advantages of their strengths and makes WCET computation scalable and amenable to hardware changes. The techniques developed were tested on standard benchmark programs from M{\"a}lardalen University and compared with results obtained from model checking methods.}, month = {September}, year = {2012}, }
Publication's urls
/publications/view.php?code=109b0e22dff205aab62a3032e6fe0b1e
/publications/view.php?code=[Kafl12]
Go back
Centre for Artificial Intelligence of UNL
Departamento de Informática, FCT/UNL
Quinta da Torre 2829-516 CAPARICA - Portugal
Tel. (+351) 21 294 8536 FAX (+351) 21 294 8541

Fundacao_FCT