Utilize este identificador para referenciar este registo: http://hdl.handle.net/10362/7968
Título: Modeling assembly program with constraints. A contribution to WCET problem
Autor: Kafle, Bishoksan
Orientador: Barahona, Pedro
Cassez, Franck
Palavras-chave: Worst Case Execution Time (WCET)
Constraint solving
Model checking
Static analysis
Data de Defesa: 2012
Editora: Faculdade de Ciências e Tecnologia
Resumo: 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 the following problems: The model checker (MC) explores exponential number of program paths irrespective of their feasibility. This limits the scalability of this method to multiple path programs. And the witness trace returned by the MC corresponding to WCET may not be feasible (executable). This may result in a solution which is not tight i.e., it overestimates the actual WCET. This thesis complements the above method with path feasibility analysis and addresses these problems. To achieve this: we first validate the witness trace returned by the MC and generate test data if it is executable. For this we generate constraints over a trace and solve a constraint satisfaction problem. Experiment shows that 33% of these traces (obtained while computing WCET on standard WCET benchmark programs) are infeasible. Second, we use constraint solving technique to compute approximate WCET solely based on the program (without taking into account the hardware characteristics), and suggest some feasible and probable worst case paths which can produce WCET. Each of these paths forms an input to the MC. The more precise WCET then can be computed on these paths using the above method. The maximum of all these is the WCET. In addition this, we provide a mechanism to compute an upper bound of over approximation for WCET computed using model checking method. This effort of combining constraint solving technique with model checking takes advantages of their strengths and makes WCET computation scalable and amenable to hardware changes. We use our technique to compute WCET on standard benchmark programs from M¨alardalen University and compare our results with results from model checking method.
Descrição: Dissertação para obtenção do Grau de Mestre em Lógica Computacional
URI: http://hdl.handle.net/10362/7968
Aparece nas colecções:FCT: DI - Dissertações de Mestrado

Ficheiros deste registo:
Ficheiro Descrição TamanhoFormato 
Kafle_2012.pdf769,22 kBAdobe PDFVer/Abrir

FacebookTwitterDeliciousLinkedInDiggGoogle BookmarksMySpace
Formato BibTex MendeleyEndnote Degois 

Todos os registos no repositório estão protegidos por leis de copyright, com todos os direitos reservados.