DC Field | Value | Language |
---|---|---|
dc.contributor.author | Lee, Jaehun | - |
dc.contributor.author | BAE, KYUNGMIN | - |
dc.contributor.author | Olveczky, Peter Csaba | - |
dc.contributor.author | Kim, Sharon | - |
dc.contributor.author | Kang, Minseok | - |
dc.date.accessioned | 2023-02-28T08:40:38Z | - |
dc.date.available | 2023-02-28T08:40:38Z | - |
dc.date.created | 2023-02-28 | - |
dc.date.issued | 2022-12 | - |
dc.identifier.issn | 1433-2779 | - |
dc.identifier.uri | https://oasis.postech.ac.kr/handle/2014.oak/116013 | - |
dc.description.abstract | This paper presents the HybridSynchAADL modeling language and formal analysis tool for virtually synchronous cyber-physical systems with complex control programs, continuous behaviors, and bounded clock skews, network delays, and execution times. We leverage the Hybrid PALS methodology, so that it is sufficient to model and verify the much simpler underlying synchronous designs. We define the HybridSynchAADL language as a sublanguage of the avionics modeling standard AADL for modeling such synchronous designs in AADL. We define the formal semantics of HybridSynchAADL using Maude with SMT solving, which allows us to represent advanced control programs and communication features in Maude, while capturing timing uncertainties and continuous behaviors symbolically with SMT solving. We have developed new general methods for optimizing the performance of such symbolic rewriting, which makes the analysis of HybridSynchAADL models feasible. We have integrated the formal modeling and analysis of HybridSynchAADL models into the OSATE tool environment for AADL. Finally, we demonstrate the effectiveness of the Hybrid PALS methodology and HybridSynchAADL on a number of applications, including autonomous drones that collaborate to achieve common goals, and compare the performance of our tool with other state-of-the-art formal tools for hybrid systems. | - |
dc.language | English | - |
dc.publisher | SPRINGER HEIDELBERG | - |
dc.relation.isPartOf | INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER | - |
dc.title | Modeling and formal analysis of virtually synchronous cyber-physical systems in AADL | - |
dc.type | Article | - |
dc.identifier.doi | 10.1007/s10009-022-00665-z | - |
dc.type.rims | ART | - |
dc.identifier.bibliographicCitation | INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER, v.24, no.6, pp.911 - 948 | - |
dc.identifier.wosid | 000849444600001 | - |
dc.citation.endPage | 948 | - |
dc.citation.number | 6 | - |
dc.citation.startPage | 911 | - |
dc.citation.title | INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER | - |
dc.citation.volume | 24 | - |
dc.contributor.affiliatedAuthor | Lee, Jaehun | - |
dc.contributor.affiliatedAuthor | BAE, KYUNGMIN | - |
dc.contributor.affiliatedAuthor | Kim, Sharon | - |
dc.contributor.affiliatedAuthor | Kang, Minseok | - |
dc.identifier.scopusid | 2-s2.0-85137520519 | - |
dc.description.journalClass | 1 | - |
dc.description.journalClass | 1 | - |
dc.description.isOpenAccess | N | - |
dc.type.docType | Article | - |
dc.subject.keywordAuthor | Cyber-physical systems | - |
dc.subject.keywordAuthor | Virtual synchrony | - |
dc.subject.keywordAuthor | AADL | - |
dc.subject.keywordAuthor | Formal methods | - |
dc.subject.keywordAuthor | Model checking | - |
dc.subject.keywordAuthor | Maude | - |
dc.subject.keywordAuthor | SMT | - |
dc.relation.journalWebOfScienceCategory | Computer Science, Software Engineering | - |
dc.description.journalRegisteredClass | scie | - |
dc.relation.journalResearchArea | Computer Science | - |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.
library@postech.ac.kr Tel: 054-279-2548
Copyrights © by 2017 Pohang University of Science ad Technology All right reserved.