滑动
发表于 2025-3-23 12:29:54
Modeling UML Template Classes with FoCaLiZerchitecture (MDA) techniques can be applied to generate code from such specifications. Because UML lacks formal basis to analyze and check model consistency, it is pertinent to choose a formal target language (in the MDA process) to enable proofs and verification techniques. To achieve this goal, we
缺陷
发表于 2025-3-23 16:35:51
Integrating Event-B Modelling and Discrete-Event Simulation to Analyse Resilience of Data Stores in ers to predict the main resilience characteristics — fault tolerance and performance — at the early design stages. In this paper, we experiment with integrating Event-B modelling with discrete-event simulation. Event-B allows us to reason about correctness and data integrity properties of data store
Infect
发表于 2025-3-23 20:02:18
Applying an Integrated Modelling Process to Run-time Management of Many-Core Systemsible impact on user experience. This paper outlines the application of a process for development of a run-time management system that integrates a range of modelling, validation, verification and generation tools at appropriate stages. We outline the models, process and tools we used to develop a te
glucagon
发表于 2025-3-24 01:36:01
Verifying Behavioral UML Systems via CEGARpted modeling language for embedded and safety critical systems. As such the correct behavior of systems represented as UML models is crucial. . is a successful automated verification technique for checking whether a system satisfies a desired property. Nevertheless, its applicability is often imped
arsenal
发表于 2025-3-24 06:10:38
http://reply.papertrans.cn/47/4686/468515/468515_15.png
征兵
发表于 2025-3-24 09:00:03
Verifying Modal Workflow Specifications Using Constraint Solvingmodal workflow specifications using constraint solving as a computational tool. Its main contribution consists in developing an innovative formal framework based on constraint systems to model executions of workflow Petri nets and their structural properties, as well as to verify their modal specifi
绕着哥哥问
发表于 2025-3-24 10:45:06
http://reply.papertrans.cn/47/4686/468515/468515_17.png
抗体
发表于 2025-3-24 15:02:32
Automated Theorem Prover Assisted Program Calculationsbersome and errorprone. To address these issues, we have developed automated theorem provers assisted program and formula transformation rules, which when coupled with the ability to extract context of a subformula, help in shortening and simplifying the derivations. We have implemented this approac
artifice
发表于 2025-3-24 22:33:52
Managing LTL Properties in Event-B Refinementerties are preserved, but additional reasoning is required in order to establish liveness and fairness properties.In this paper we present results which allow a closer integration of two formal methods, Event-B and linear temporal logic. In particular we show how a class of temporal logic properties
纵火
发表于 2025-3-24 23:30:25
http://reply.papertrans.cn/47/4686/468515/468515_20.png