Search results for "formal methods"
showing 5 items of 15 documents
Survey of Formal Verification Methods for Smart Contracts on Blockchain
2019
Due to the immutable nature of distributed ledger technology such as blockchain, it is of utter importance that a smart contract works as intended before employment outside test network. This is since any bugs or errors will become permanent once published to the live network, and could lead to substantial economic losses; as manifested in the infamous DAO smart contract exploit hack in 2016. In order to avoid this, formal verification methods can be used to ensure that the contract behaves according to given specifications. This paper presents a survey of the state of the art of formal verification of smart contracts. Being a relatively new research area, a standard or best practice for fo…
Formal Modeling and Discrete-Time Analysis of BPEL Web Services
2008
International audience; Web services are increasingly used for building enterprise information systems according to the Service Oriented Architecture (SOA) paradigm. We propose in this paper a tool-equipped methodology allowing the formal modeling and analysis of Web services described in the BPEL language. The discrete-time transition systems modeling the behavior of BPEL descriptions are obtained by an exhaustive simulation based on a formalization of BPEL semantics using the Algebra of Timed Processes (ATP). These models are then analyzed by model checking value-based temporal logic properties using the CADP toolbox. The approach is illustrated with the design of a Web service for GPS na…
Extending CSG with projections: Towards formally certified geometric modeling
2015
We extend traditional Constructive Solid Geometry (CSG) trees to support the projection operator. Existing algorithms in the literature prove various topological properties of CSG sets. Our extension readily allows these algorithms to work on a greater variety of sets, in particular parametric sets, which are extensively used in CAD/CAM systems. Constructive Solid Geometry allows for algebraic representation which makes it easy for certification tools to apply. A geometric primitive may be defined in terms of a characteristic function, which can be seen as the zero-set of a corresponding system along with inequality constraints. To handle projections, we exploit the Disjunctive Normal Form,…
Supporting Agile Development by Facilitating Natural User Interaction with Executable Formal Specifications
2011
Agile development benefits from fast feedback from various stakeholders. If implemented in a suitable way, formal methods can enhance the agile development process. With an executable formal specification, it is possible to analyse and simulate the behaviour of the target system before it is being built. However, for the users' and developers' natural participation in the development process, it is necessary to use a real end-user interface and bind it to the execution environment being used in the simulations and animations. This requires, though, that the execution model used to simulate the specification is appropriately changed to facilitate the use of these user interfaces. The authors…
Formal specification of open standards and the case of RSS v2.0
2014
Open standardization seems to be very popular among software developers as it makes the standard's adoption by the software engineering community easier and smoother. Formal specification methods, on the other hand, while very promising, are being adopted by protocol engineers very slowly; the industry seems to have little motivation to move into this, almost unknown, territory.In this paper the authors present the i) idea of applying formal methods (formal specification techniques) to open standards' specifications, and ii) an example of a formal specification of open standards, RSS v2.0 in particular. The authors support and provide evidence for the advantages of the open standards formal…