Strength
发表于 2025-3-23 10:49:38
Refinement of Finite State Machines with Complementary Model Checking,sforms models into B language code for efficient application of theorem proving. Refinement and verification is performed across three levels with the B-Method and with complementary verification through the RAVEN model checker. The presented methodology is outlined by the example of an echo cancellation unit in Chapter 14.
Flustered
发表于 2025-3-23 17:51:41
http://reply.papertrans.cn/95/9401/940066/940066_12.png
聪明
发表于 2025-3-23 20:24:27
http://reply.papertrans.cn/95/9401/940066/940066_13.png
magnate
发表于 2025-3-24 00:29:39
https://doi.org/10.1007/978-1-4020-2867-0Embedded System; Hardware; Hardwarebeschreibungssprache; Interface; SoC; Software; SystemC; Unified Modelin
Albinism
发表于 2025-3-24 02:20:51
The UML-B Profile for Formal Systems Modelling in UML,hieve this Integration we have specialised UML modelling elements via stereotypes, added tagged values to represent B modelling features and imposed constraints to ensure that UML-B modeis are translated into usable B. Here we describe ongoing work to define UML-B as a profile in accordance with the UML extensibility mechanisms.
antidote
发表于 2025-3-24 07:05:04
BHDL: Principles and tools for generating proven hardware,ible as an actual implementation is approached. This means that the initial refinement steps ued in hardware are, in principle, also pplicable to software, and vice versa..The subset of the B-language that serves to describe hardware is called BHDL. The definition of the BHDL subset is oriented at the register level for hardware description.
cylinder
发表于 2025-3-24 12:59:35
http://reply.papertrans.cn/95/9401/940066/940066_17.png
BAIL
发表于 2025-3-24 18:42:36
Embedded System Design Using the PUSSEE Method,ery phase of the co-design cycle. The main idea is to build fully functional System modeis that are formally proven to be correct, and based on them to produce automatically the hardware and the Software parts of the System. The approach presented relies on the combined use of UML and B language.
Fatten
发表于 2025-3-24 19:40:44
U2B,efits that they offer. In previous work, we have proposed an integration of UML and the formal notation, B called UML-B. The integrated modelling notation, UML-B, inherits from both UML and B but primarily, is a specialisation of the UML. Here we describe how UML-B can be used to obtain a useful translation into B using the U2B translation tool.
homeostasis
发表于 2025-3-25 02:10:51
The Echo Cancellation Unit Case Study, cancellation unit of a mobile phone with the Atelier-B toolkit and the RAVEN model checker. The experimental results show that the presented methodology requires almost no user interaction and gives acceptable runtimes with Atelier-B.