## Abstrakt

The idea of analysing real programs by process algebraic

methods probably goes back to the Occam language using the CSP

process algebra [43]. In [16,24] Degano et al. followed in that tradition

by analysing Mobile Agent Programs written in the Higher Order Functional,

Concurrent and Distributed, programming language Facile [47],

by equipping Facile with a process algebraic semantics based on true concurrency.

This semantics facilitated analysis of programs revealing subtle

bugs that would otherwise be very hard to find. Inspired by the idea of

translating real programs into process algebraic frameworks, we have in

recent years pursued an agenda of translating hard-real-time embedded

safety critical programs written in the Safety Critical Java Profile [33]

into networks of timed automata [4] and subjecting those to automated

analysis using the UPPAAL model checker [10]. Several tools have been

built and the tools have been used to analyse a number of systems for

properties such as worst case execution time, schedulability and energy

optimization [12–14,19,34,36,38]. In this paper we will elaborate on the

theoretical underpinning of the translation from Java programs to timed

automata models and briefly summarize some of the results based on this

translation. Furthermore, we discuss future work, especially relations to

the work in [16,24] as Java recently has adopted first class higher order

functions in the form of lambda abstractions.

methods probably goes back to the Occam language using the CSP

process algebra [43]. In [16,24] Degano et al. followed in that tradition

by analysing Mobile Agent Programs written in the Higher Order Functional,

Concurrent and Distributed, programming language Facile [47],

by equipping Facile with a process algebraic semantics based on true concurrency.

This semantics facilitated analysis of programs revealing subtle

bugs that would otherwise be very hard to find. Inspired by the idea of

translating real programs into process algebraic frameworks, we have in

recent years pursued an agenda of translating hard-real-time embedded

safety critical programs written in the Safety Critical Java Profile [33]

into networks of timed automata [4] and subjecting those to automated

analysis using the UPPAAL model checker [10]. Several tools have been

built and the tools have been used to analyse a number of systems for

properties such as worst case execution time, schedulability and energy

optimization [12–14,19,34,36,38]. In this paper we will elaborate on the

theoretical underpinning of the translation from Java programs to timed

automata models and briefly summarize some of the results based on this

translation. Furthermore, we discuss future work, especially relations to

the work in [16,24] as Java recently has adopted first class higher order

functions in the form of lambda abstractions.

Originalsprog | Engelsk |
---|---|

Titel | Programming Languages with Applications to Biology and Security : Essays Dedicated to Pierpaolo Degano on the Occasion of His 65th Birthday |

Redaktører | Chiara Bodei, Gian-Luigi Ferrari , Corrado Priami |

Antal sider | 20 |

Forlag | Springer |

Publikationsdato | 2015 |

Sider | 319-338 |

ISBN (Trykt) | 978-3-319-25526-2 |

ISBN (Elektronisk) | 978-3-319-25527-9 |

DOI | |

Status | Udgivet - 2015 |

Navn | Lecture Notes in Computer Science |
---|---|

Nummer | 9465 |

ISSN | 0302-9743 |