Design and Verification of Cyber-Physical Systems Specified by Petri Nets—A Case Study of a Direct Matrix Converter
| Autor: | Remigiusz Wisniewski, Grzegorz Bazydlo, Iwona Grobelna, Marcin Wojnakowski, Paweł Szcześniak |
|---|---|
| Jazyk: | angličtina |
| Rok vydání: | 2019 |
| Předmět: |
Computer science
General Mathematics SVM design 0211 other engineering and technologies 02 engineering and technology cyber-physical system 0202 electrical engineering electronic engineering information engineering Computer Science (miscellaneous) Commutation Design methods Engineering (miscellaneous) computer.programming_language 021103 operations research direct matrix converter lcsh:Mathematics 020208 electrical & electronic engineering Hardware description language Cyber-physical system Petri net lcsh:QA1-939 Support vector machine Computer engineering verification computer Space vector modulation Software verification |
| Zdroj: | Mathematics, Vol 7, Iss 9, p 812 (2019) Mathematics Volume 7 Issue 9 |
| ISSN: | 2227-7390 |
| Popis: | The paper proposes a novel design technique of cyber-physical systems (CPSs). The system is specified by a Petri net, and further modelled in a hardware description language (HDL) towards final implementation in a programmable device. Contrary to the traditional design methods, the proposed solution is highly focused on the verification aspects. The system is checked three times before the final implementation in hardware. Initially, the Petri-net based specification is formally verified by the application of the model-checking technique. Secondly, software verification of the modelled system is performed. Finally, the hardware verification of the already implemented system is executed. The proposed method is explained by an example of a direct matrix converter (MC) with transistor commutation and space vector modulation (SVM). The main benefits, as well as the limitations, of the proposed solution are discussed and analysed. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
| Nepřihlášeným uživatelům se plný text nezobrazuje | K zobrazení výsledku je třeba se přihlásit. |