Formal Aspects of Computing
Công bố khoa học tiêu biểu
* Dữ liệu chỉ mang tính chất tham khảo
Sắp xếp:
Active learning for extended finite state machines
Formal Aspects of Computing - Tập 28 - Trang 233-263 - 2016
We present a black-box active learning algorithm for inferring extended finite state machines (EFSM)s by dynamic black-box analysis. EFSMs can be used to model both data flow and control behavior of software and hardware components. Different dialects of EFSMs are widely used in tools for model-based software development, verification, and testing. Our algorithm infers a class of EFSMs called regi......
Multitraces, hypertraces and partial order semantics
Formal Aspects of Computing - Tập 4 - Trang 649-672 - 1992
In this paper, we consider a generalisation of a result due to the author which describes the way in which Mazurkiewicz trace languages serve to represent systems of labelled partial orders, as used in non-interleaving semantics of parallelism. The generalisation extends the class of partial order systems to exclude only a form of non-determinism. Their representation is in terms ofa generalisatio......
Dynamical Quantities in Net Systems
Formal Aspects of Computing - Tập 14 - Trang 55-89 - 2002
The paper presents some known material of higher-level Petri nets in analogy to the dynamics of physical systems. Its aim is to widen the view on the role of the incidence matrix in the analysis of net systems. Rather than focusing on constant state quantities (S-invariants) and cyclic actions (T-invariants), i.e. on solutions of the homogeneous equation systems based on the incidence matrix, it ......
Property-directed incremental invariant generation
Formal Aspects of Computing - Tập 20 - Trang 379-405 - 2008
A fundamental method of analyzing a system such as a program or a circuit is invariance analysis, in which one proves that an assertion holds on all reachable states. Typically, the proof is performed via induction; however, an assertion, while invariant, may not be inductive (provable via induction). Invariant generation procedures construct auxiliary inductive assertions for strengthening the as......
GR(1)*: GR(1) specifications extended withexistential guaranteesAbstract
Reactive synthesis is an automated procedure to obtain a
correct-by-construction reactive system from its temporal logic
specification. GR(1) is an expressive assume-guarantee fragment of
LTL that enables efficient synthesis and has been recently used in
different contexts and application domains. A common form of
providing system's requirements ... ...
Formal Aspects of Computing - - 2021
Dynamic intransitive noninterference revisited
Formal Aspects of Computing - Tập 29 - Trang 1087-1120 - 2017
The paper studies dynamic information flow security policies in an automaton-based model. Two semantic interpretations of such policies are developed, both of which generalize the notion of TA-security [van der Meyden ESORICS 2007] for static intransitive noninterference policies. One of the interpretations focuses on information flows permitted by policy edges, the other focuses on prohibitions i......
Typed context awareness Ambient Calculus for pervasive applications
Formal Aspects of Computing - Tập 27 - Trang 885-916 - 2015
The idea of pervasive computing is that information processing will become part of everyday life, and will be available everywhere, making computing so natural to the point of being invisible in the ambient. An important concept that arises with pervasive computing is context awareness. Context is any information that can be used to characterize an entity. Based on contextual information, applicat......
Soundness of workflow nets: classification, decidability, and analysis
Formal Aspects of Computing - Tập 23 - Trang 333-363 - 2010
Workflow nets, a particular class of Petri nets, have become one of the standard ways to model and analyze workflows. Typically, they are used as an abstraction of the workflow that is used to check the so-called soundness property. This property guarantees the absence of livelocks, deadlocks, and other anomalies that can be detected without domain knowledge. Several authors have proposed alternat......
Deductive verification of alternating systems
Formal Aspects of Computing - Tập 20 - Trang 507-560 - 2008
Alternating systems are models of computer programs whose behavior is governed by the actions of multiple agents with, potentially, different goals. Examples include control systems, resource schedulers, security protocols, auctions and election mechanisms. Proving properties about such systems has emerged as an important new area of study in formal verification, with the development of logical fr......
Tổng số: 714
- 1
- 2
- 3
- 4
- 5
- 6
- 10