English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Most formal methods see the correctness of a software system as a binarydecision. However, proving the correctness of complex systems completely isdifficult because they are composed of multiple components, usage scenarios,and environments. We present QuAC, a modular approach for quantifying thecorrectness of service-oriented software systems by combining softwarearchitecture modeling with deductive verification. Our approach is based on amodel of the service-oriented architecture and the probabilistic usagescenarios of the system. The correctness of a single service is approximated bya coverage region, which is a formula describing which inputs for that serviceare proven to not lead to an erroneous execution. The coverage regions can bedetermined by a combination of various analyses, e.g., formal verification,expert estimations, or testing. The coverage regions and the software model arethen combined into a probabilistic program. From this, we can compute theprobability that under a given usage profile no service is called outside itscoverage region. If the coverage region is large enough, then instead ofattempting to get 100% coverage, which may be prohibitively expensive, run-timeverification or testing approaches may be used to deal with inputs outside thecoverage region. We also present an implementation of QuAC for Java using themodeling tool Palladio and the deductive verification tool KeY. We demonstrateits usability by applying it to a software simulation of an energy system.

Quantifying Software Correctness by Combining Architecture Modeling and Formal Program Analysis