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 s...
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 guarantees
Formal Aspects of Computing - - 2021
Abstract 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 is through use cases,
which are existential...
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ố: 713
- 1
- 2
- 3
- 4
- 5
- 6
- 10