Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userFrom Design Contracts to Component Requirements Verification
133
0
0.0
(
0
)
Added by
Jing (Janet) Liu
Publication date
2016
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
During the development and verification of complex airborne systems, a variety of languages and development environments are used for different levels of the system hierarchy. As a result, there may be manual steps to translate requirements between these different environments. This paper presents a tool-supported export technique that translates high-level requirements from the software architecture modeling environment into observers of requirements that can be used for verification in the software component environment. This allows efficient verification that the component designs comply with their high-level requirements. It also provides an automated tool chain supporting formal verification from system requirements down to low-level software requirements that is consistent with certification guidance for avionics systems. The effectiveness of the technique has been evaluated and demonstrated on a medical infusion pump and an aircraft wheel braking system.
rate research
Read More
Design creativity, the originality and practicality of a solution concept is critical for the success of many software projects. However, little research has investigated the relationship between the way desiderata are presented and design creativity. This study therefore investigates the impact of presenting desiderata as ideas, requirements or prioritized requirements on design creativity. Two between-subjects randomized controlled experiments were conducted with 42 and 34 participants. Participants were asked to create design concepts from a list of desiderata. Participants who received desiderata framed as requirements or prioritized requirements created designs that are, on average, less original but more practical than the designs created by participants who received desiderata framed as ideas. This suggests that more formal, structured presentations of desiderata are less appropriate where a creative solution is desired. The results also show that design performance is highly susceptible to minor changes in the vernacular used to communicate desiderata.
Prototyping is an effective and efficient way of requirement validation to avoid introducing errors in the early stage of software development. However, manually developing a prototype of a software system requires additional efforts, which would increase the overall cost of software development. In this paper, we present an approach with a developed tool to automatic generation of prototypes from formal requirements models. A requirements model consists of a use case diagram, a conceptual class diagram, use case definitions specified by system sequence diagrams and the contracts of their system operations. We propose a method to decompose a contract into executable parts and non-executable parts. A set of transformation rules is given to decompose the executable part into pre-implemented primitive operations. A non-executable part is usually realized by significant algorithms such as sorting a list, finding the shortest path or domain-specific computation. It can be implemented manually or by using existing code. A CASE tool is developed that provides an interface for developers to develop a program for each non-executable part of a contract, and automatically transforms the executables into sequences of pre-implemented primitive operations. We have conducted four cases studies with over 50 use cases. The experimental result shows that the 93.65% of requirement specifications are executable, and only 6.35% are non-executable such as sorting and event-call, which can be implemented by developers manually or invoking the APIs of advanced algorithms in Java library. The one second generated the prototype of a case study requires approximate nine hours manual implementation by a skilled programmer. Overall, the result is satisfiable, and the proposed approach with the developed CASE tool can be applied to the software industry for requirements engineering.
Software verification of evolving systems is challenging mainstream methodologies and tools. Formal verification techniques often conflict with the time constraints imposed by change management practices for evolving systems. Since changes in these systems are often local to restricted parts, an incremental verification approach could be beneficial. This paper introduces SiDECAR, a general framework for the definition of verification procedures, which are made incremental by the framework itself. Verification procedures are driven by the syntactic structure (defined by a grammar) of the system and encoded as semantic attributes associated with the grammar. Incrementality is achieved by coupling the evaluation of semantic attributes with an incremental parsing technique. We show the application of SiDECAR to the definition of two verification procedures: probabilistic verification of reliability requirements and verification of safety properties.
Ethereum has become a widely used platform to enable secure, Blockchain-based financial and business transactions. However, many identified bugs and vulnerabilities in smart contracts have led to serious financial losses, which raises serious concerns about smart contract security. Thus, there is a significant need to better maintain smart contract code and ensure its high reliability. In this research: (1) Firstly, we propose an automated deep learning based approach to learn structural code embeddings of smart contracts in Solidity, which is useful for clone detection, bug detection and contract validation on smart contracts. We apply our approach to more than 22K solidity contracts collected from the Ethereum blockchain, results show that the clone ratio of solidity code is at around 90%, much higher than traditional software. We collect a list of 52 known buggy smart contracts belonging to 10 kinds of common vulnerabilities as our bug database. Our approach can identify more than 1000 clone related bugs based on our bug databases efficiently and accurately. (2) Secondly, according to developers feedback, we have implemented the approach in a web-based tool, named SmartEmbed, to facilitate Solidity developers for using our approach. Our tool can assist Solidity developers to efficiently identify repetitive smart contracts in the existing Ethereum blockchain, as well as checking their contract against a known set of bugs, which can help to improve the users confidence in the reliability of the contract. We optimize the implementations of SmartEmbed which is sufficient in supporting developers in real-time for practical uses. The Ethereum ecosystem as well as the individual Solidity developer can both benefit from our research.
Smart contracts have been increasingly used together with blockchains to automate financial and business transactions. However, many bugs and vulnerabilities have been identified in many contracts which raises serious concerns about smart contract security, not to mention that the blockchain systems on which the smart contracts are built can be buggy. Thus, there is a significant need to better maintain smart contract code and ensure its high reliability. In this paper, we propose an automated approach to learn characteristics of smart contracts in Solidity, which is useful for clone detection, bug detection and contract validation on smart contracts. Our new approach is based on word embeddings and vector space comparison. We parse smart contract code into word streams with code structural information, convert code elements (e.g., statements, functions) into numerical vectors that are supposed to encode the code syntax and semantics, and compare the similarities among the vectors encoding code and known bugs, to identify potential issues. We have implemented the approach in a prototype, named SmartEmbed. Results show that our tool can effectively identify many repetitive instances of Solidity code, where the clone ratio is around 90%. Code clones such as type-III or even type-IV semantic clones can also be detected accurately. Our tool can identify more than 1000 clone related bugs based on our bug databases efficiently and accurately. Our tool can also help to efficiently validate any given smart contract against a known set of bugs, which can help to improve the users confidence in the reliability of the contract. The anonymous replication packages can be accessed at: https://drive.google.com/file/d/1kauLT3y2IiHPkUlVx4FSTda-dVAyL4za/view?usp=sharing, and evaluated it with more than 22,000 smart contracts collected from the Ethereum blockchain.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
