Towards automatic program specification using SME models

Publikation: Bidrag til bog/antologi/rapportKonferencebidrag i proceedingsForskningfagfællebedømt

  • Alberte Thegler
  • Mads Ohm Larsen
  • Kenneth Skovhede
  • Brian Vinter

This paper introduces a method to simplify hardware modeling and verification there of in order for software programmers to, more easily, meet the demands of the growing embedded device industry. We describe a simple method for transpiling from the new SME Implementation Language into CSPM and using formal verification to verify properties within the generated program. We present a small example consisting of a seven segment display clock network and introduce how to verify the widths of the channels in the network.

OriginalsprogEngelsk
TitelCommunicating Process Architectures 2017 and 2018, WoTUG-39 and WoTUG-40 - Proceedings of CPA 2017 (WoTUG-39) and Proceedings of CPA 2018 (WoTUG-40)
RedaktørerJan Baekgaard Pedersen, Kevin Chalmers, Jan F. Broenink, Brian Vinter, Kevin Vella, Peter H. Welch, Marc L. Smith, Kenneth Skovhede
Antal sider16
ForlagIMIA and IOS Press
Publikationsdato2019
Sider415-430
ISBN (Elektronisk)9781614999485
DOI
StatusUdgivet - 2019
Begivenhed39th WoTUG Conference on Communicating Process Architectures, CPA 2017 and 40th WoTUG Conference on Communicating Process Architectures, CPA 2018 - Dresden, Tyskland
Varighed: 19 aug. 201822 aug. 2018

Konference

Konference39th WoTUG Conference on Communicating Process Architectures, CPA 2017 and 40th WoTUG Conference on Communicating Process Architectures, CPA 2018
LandTyskland
ByDresden
Periode19/08/201822/08/2018
NavnConcurrent Systems Engineering Series
Vol/bind70
ISSN1383-7575

ID: 241090930