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 Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

System development is not a linear, one-shot process. It proceeds throughrefinements and revisions. To support assurance that the system satisfies itsrequirements, it is desirable that continuous verification can be performedafter each refinement or revision step. To achieve practical adoption, formalsystem modeling and verification must accommodate continuous verificationefficiently and effectively. Our proposal to address this problem is TOrPEDO, averification approach where models are given via Partial Kripke Structures(PKSs) and requirements are specified as Linear-time Temporal Logic (LTL)properties. PKSs support refinement, by deliberately indicating unspecifiedparts of the model that are later completed. We support verification in twocomplementary forms: via model checking and proofs. Model checking is useful toprovide counterexamples, i.e., pinpoint model behaviors that violaterequirements. Proofs are instead useful since they can explain why requirementsare satisfied. In our work, we introduce a specific concept of proof, calledtopological proof (TP). A TP produces a slice of the original PKS whichjustifies the property satisfaction. Because models can be incomplete, TOrPEDOsupports reasoning on requirements satisfaction, violation, and possiblesatisfaction (in the case where the satisfaction depends on unknown parts).

Integrating Topological Proofs with Model Checking to Instrument Iterative Design