Loading...
Please wait, while we are loading the content...
Similar Documents
Electronic Communications of the EASST Volume 53 ( 2012 ) Proceedings of the 12 th International Workshop on Automated Verification of Critical Systems ( AVoCS 2012 ) Optimized Transformation and Verification of SystemC Methods
| Content Provider | Semantic Scholar |
|---|---|
| Author | Pockrandt, Marcel Herber, Paula Gross, Holger Glesner, Sabine |
| Copyright Year | 2012 |
| Abstract | Concurrent designs can be automatically verified by transforming them into an automata-based representation and by model checking the resulting model. However, when transforming a concurrent design into an automata-based representation, each method has to be translated into a single automaton. This produces a significant overhead for model checking. In this paper, we present an optimization of our previously proposed transformation from SystemC into UPPAAL timed automata. The main idea is that we analyze whether SystemC methods can be executed atomically and then we use the results for generating a reduced automata model. We have implemented the optimized transformation in our SystemC to Timed Automata Transformation Engine (STATE) and demonstrate the effect of our optimization with experimental results from micro benchmarks, a simple producer-consumer example, and from an Anti-Slip Regulation and Anti-lock Braking System (ASR/ABS). |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | https://journal.ub.tu-berlin.de/eceasst/article/download/789/788 |
| Alternate Webpage(s) | http://journal.ub.tu-berlin.de/eceasst/article/download/789/788 |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
