SystemC används i stor utsträckning för modellering och simulering inom hårdvara/programvara samdesign. På grund av bristen på en komplett formell semantik, är det inte möjligt att verifiera SystemC konstruktioner. I detta dokument presenterar vi en strategi för att övervinna detta problem genom att definiera semantiken i SystemC genom en kartläggning från SystemC-konstruktioner till de väldefinierade semantikerna i Uppaal timed automata. Det informellt definierade beteendet och strukturen för SystemC-konstruktioner är helt bevarade i de genererade Uppaal-modellerna. De resulterande Uppaal-modellerna gör det möjligt för oss att använda Uppaal-modellens checker och verktygssviten Uppaal, inklusive simulerings- och visualiseringsverktyg. Modellkontrollen kan användas för att verifiera viktiga egenskaper som liv, dödlägesfrihet eller överensstämmelse med tidsbegränsningar. Vi har genomfört den presenterade omvandlingen, tillämpat den på två exempel och verifierat liv, säkerhet och timing egenskaper genom modellkontroll, vilket visar tillämpligheten av vår strategi i praktiken.
I REF har en metodkartläggning SystemC designar in i UPAAL tidsinställd automata föreslagits.
Model checking SystemC designs using timed automata
{'venue': "CODES+ISSS '08", 'journal': None, 'mag_field_of_study': ['Computer Science']}