Zobrazeno 1 - 10
of 25
pro vyhledávání: '"Alvaro Miyazawa"'
Publikováno v:
Frontiers in Robotics and AI, Vol 9 (2022)
The need for robotic systems to be verified grows as robots are increasingly used in complex applications with safety implications. Model-driven engineering and domain-specific languages (DSLs) have proven useful in the development of complex systems
Externí odkaz:
https://doaj.org/article/00798d6389ad4c42a9c8ddf4ff0db92a
Autor:
Alvaro Miyazawa, Ana Cavalcanti
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 209, Iss Proc. Refine 2015, Pp 71-86 (2016)
Safety-Critical Java (SCJ) is a version of Java whose goal is to support the development of real-time, embedded, safety-critical software. In particular, SCJ supports certification of such software by introducing abstractions that enforce a simpler a
Externí odkaz:
https://doaj.org/article/3c090268be31432b92344b025d68656b
Autor:
Ana Cavalcanti, Alvaro Miyazawa
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 55, Iss Proc. Refine 2011, Pp 65-83 (2011)
Simulink/Stateflow charts are widely used in industry for the specification of control systems, which are often safety-critical. This suggests a need for a formal treatment of such models. In previous work, we have proposed a technique for automatic
Externí odkaz:
https://doaj.org/article/5a007793a0304c5cb10ea6d4fea2386f
Publikováno v:
Software and Systems Modeling. 21:667-716
RoboChart is a timed domain-specific language for robotics, distinctive in its support for automated verification by model checking and theorem proving. Since uncertainty is an essential part of robotic systems, we present here an extension to RoboCh
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::3cf2ad949677721f83b117b3fafcc92f
https://doi.org/10.1007/s10270-021-00916-8
https://doi.org/10.1007/s10270-021-00916-8
Publikováno v:
Science of Computer Programming. 181:140-176
Safety-Critical Java (SCJ) is a version of Java for real-time, embedded, safety-critical applications. It supports certification via abstractions that enforce a particular program architecture, with controlled concurrency and memory models. SCJ is an
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::b32c156c2f9308bef050827ad87c159e
https://doi.org/10.1016/j.scico.2019.01.002
https://doi.org/10.1016/j.scico.2019.01.002
Autor:
Wei Li, Ana Cavalcanti, Alvaro Miyazawa, André Didier, Jon Timmis, Madiel Conserva Filho, Augusto Sampaio, Pedro Ribeiro
Publikováno v:
Science of Computer Programming. 174:1-37
Simulation is a favoured technique for analysis of robotic systems. Currently, however, simulations are programmed in an ad hoc way, for specific simulators, using either proprietary languages or general languages like C or C++. Even when a higher-le
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::fd549da40fc2732e8bc91104a86d112d
https://doi.org/10.1016/j.scico.2019.01.004
https://doi.org/10.1016/j.scico.2019.01.004
Autor:
Alvaro Miyazawa, James Baxter, Ana Cavalcanti, Gustavo Carvalho, Augusto Sampaio, Madiel Conserva Filho, Pedro Ribeiro, Will Barnett
Publikováno v:
Software Engineering for Robotics ISBN: 9783030664930
Simulation is favored by roboticists to evaluate controller design and software. Often, state machines are drawn to convey overall ideas and used as a basis to program tool-specific simulations. The simulation code, written in general or proprietary
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::4be8d99157248d3ef0e90d45c7dc1a2b
https://doi.org/10.1007/978-3-030-66494-7_9
https://doi.org/10.1007/978-3-030-66494-7_9
Publikováno v:
Formal Aspects of Component Software ISBN: 9783030021450
FACS
FACS
State-machine based notations are ubiquitous in the description of component systems, particularly in the robotic domain. To ensure these systems are safe and predictable, formal verification techniques are important, and can be cost-effective if the
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::4ea4b9ca172936829c7dd606290c372d
https://doi.org/10.1007/978-3-030-02146-7_7
https://doi.org/10.1007/978-3-030-02146-7_7
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783319989372
IFM
IFM
RoboChart is a graphical domain-specific language, based on UML, but tailored for the modelling and verification of single robot systems. In this paper, we introduce RoboChart facilities for modelling and verifying heterogeneous collections of intera
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::d6392b64801984758ec23f04cac09a8b
https://doi.org/10.1007/978-3-319-98938-9_1
https://doi.org/10.1007/978-3-319-98938-9_1
Publikováno v:
Distributed Autonomous Robotic Systems ISBN: 9783319730066
DARS
DARS
Controllers for autonomous robotic systems can be specified using state machines . However, these are typically developed in an ad hoc manner without formal semantics, which makes it difficult to analyse the controller. Simulations are often used dur
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::2cb07914f76c2c2d664b58c7e47b53fa
https://doi.org/10.1007/978-3-319-73008-0_36
https://doi.org/10.1007/978-3-319-73008-0_36