A DEVS-based pivotal modeling formalism and its verification and validation framework
| dc.rights.license | open | en_US |
| dc.contributor.author | SAMUEL, Kehinde G. | |
| dc.contributor.author | BOUARE, Nourou-Dine M. | |
| dc.contributor.author | MAÏGA, Oumar | |
| hal.structure.identifier | Laboratoire de l'intégration, du matériau au système [IMS] | |
| dc.contributor.author | TRAORE, Mamadou Kaba
IDREF: 112136893 | |
| dc.date.accessioned | 2021-03-23T15:14:09Z | |
| dc.date.available | 2021-03-23T15:14:09Z | |
| dc.date.issued | 2020-09-26 | |
| dc.identifier.issn | 0037-5497 | en_US |
| dc.identifier.uri | oai:crossref.org:10.1177/0037549720958056 | |
| dc.identifier.uri | https://oskar-bordeaux.fr/handle/20.500.12278/26791 | |
| dc.description.abstractEn | System verification is an ever-lasting system engineering challenge. The increasing complexity in system simulation requires some level of expertise in handling the idioms of logic and discrete mathematics to correctly drive a full verification process. It is recognized that visual modeling can help to fill the knowledge gap between system experts and analysis experts. However, such an approach has been used on the one hand to specify the behavior of complex systems, and on the other hand to specify complex requirement properties, but not simultaneously. This paper proposes a framework that is unique in supporting a full system verification process based on the graphical modeling of both the system of interest and the requirements to be checked. Patterns are defined to transform the resulting models to formal specifications that a model checker can manipulate. A real-time crossing system is used to illustrate the proposed framework. | |
| dc.language.iso | EN | en_US |
| dc.source | crossref | |
| dc.subject.en | High Level Language for Systems Specification (HiLLS) | |
| dc.subject.en | Discrete Event System Specification (DEVS) | |
| dc.subject.en | formal verification | |
| dc.subject.en | temporal logic | |
| dc.subject.en | model transformation | |
| dc.subject.en | UPPAAL | |
| dc.title.en | A DEVS-based pivotal modeling formalism and its verification and validation framework | |
| dc.type | Article de revue | en_US |
| dc.identifier.doi | 10.1177/0037549720958056 | |
| dc.subject.hal | Informatique [cs]/Modélisation et simulation | en_US |
| bordeaux.journal | SIMULATION | en_US |
| bordeaux.page | 969-992 | en_US |
| bordeaux.volume | 96 | en_US |
| bordeaux.hal.laboratories | Laboratoire d’Intégration du Matériau au Système (IMS) - UMR 5218 | en_US |
| bordeaux.issue | 12 | en_US |
| bordeaux.institution | Université de Bordeaux | en_US |
| bordeaux.institution | Bordeaux INP | en_US |
| bordeaux.peerReviewed | oui | en_US |
| bordeaux.inpress | non | en_US |
| bordeaux.import.source | dissemin | |
| hal.identifier | hal-03178210 | |
| hal.version | 1 | |
| hal.date.transferred | 2021-03-23T15:18:56Z | |
| hal.export | false | |
| workflow.import.source | dissemin | |
| bordeaux.COinS | ctx_ver=Z39.88-2004&rft_val_fmt=info:ofi/fmt:kev:mtx:journal&rft.jtitle=SIMULATION&rft.date=2020-09-26&rft.volume=96&rft.issue=12&rft.spage=969-992&rft.epage=969-992&rft.eissn=0037-5497&rft.issn=0037-5497&rft.au=SAMUEL,%20Kehinde%20G.&BOUARE,%20Nourou-Dine%20M.&MA%C3%8FGA,%20Oumar&TRAORE,%20Mamadou%20Kaba&rft.genre=article |
