Coronary-Spasm 发表于 2025-3-26 20:59:10
Composition and refinement in the B-method,ossibly introduced by composition primitives . and .. We exhibit local conditions on components which are sufficient to ensure global correctness of a software system. Finally, we show how restrictions on the architecture of software systems may guarantee these conditions.条街道往前推 发表于 2025-3-27 01:26:59
http://reply.papertrans.cn/20/1930/192953/192953_32.png体贴 发表于 2025-3-27 07:21:26
Introducing dynamic constraints in B,n different complementary ways, how a system is allowed to evolve. Such descriptions are independent of the proposed evolutions of the system, which are defined, as usual, by means of a number of operations. Some proof obligations are thus proposed in order to reconcile the two points of view. We haForegery 发表于 2025-3-27 12:57:43
Retrenchment: An engineering variation on refinement, describe all but a fraction of many realistic developments. An alternative notion is proposed called retrenchment, which allows information to migrate between I/O and state aspects of operations at different levels of abstraction, and which allows only a fraction of the high level behaviour to be c大火 发表于 2025-3-27 17:00:49
Synthesising structure from flat specifications, and also as a first step of the refinement process. Whilst the structuring mechanisms available in the B method are well-suited for the latter purpose, the rich type constructions of VDM are useful for the former..In this paper we propose a method which synthesises a structured B design from a flatGNAW 发表于 2025-3-27 19:32:08
An object-based approach to the B formal method, formal method. Our goal is to retain some OOM advantages and produce a flexible and reliable specification, and through the use of our example, we show how this is achieved. We prove formally that our design meets its informal specification with the help of B-Toolkit Release 3.3.1. We illustrate th商议 发表于 2025-3-28 00:16:37
http://reply.papertrans.cn/20/1930/192953/192953_37.pngneologism 发表于 2025-3-28 04:44:26
Process control engineering: Contribution to a formal structuring framework with the B method, is shown how the B method can be used to define implementation independent modular specifications. Benefits are related to the re-use of verified and perennial specifications for control systems facing a fast evolution of implementation technologies. Limits are related to the compliance of formal m婴儿 发表于 2025-3-28 06:30:28
http://reply.papertrans.cn/20/1930/192953/192953_39.pngemission 发表于 2025-3-28 10:57:06
Abstract state machines: Designing distributed systems with state machines and B,ata state. The behavioural states are shown on a state diagram, whose transitions are labelled with an “event” and a B operation. The firing of a transition is synonymous with the occurrence of its associated event. We use a synchronous model of communication based on shared events which simultaneou