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:
Translating FSP into LOTOS and networks of automata
Formal Aspects of Computing - Tập 22 - Trang 681-711 - 2009
Many process calculi have been proposed since Robin Milner and Tony Hoare opened the way more than 25 years ago. Although they are based on the same kernel of operators, most of them are incompatible in practice. We aim at reducing the gap between process calculi, and especially making possible the joint use of underlying tool support. Finite state processes (FSP) is a widely used calculus equippe...... hiện toàn bộ
Read atomic transactions with prevention of lost updates: ROLA and its formal analysis
Formal Aspects of Computing - Tập 31 - Trang 503-540 - 2019
Designers of distributed database systems face the choice between stronger consistency guarantees and better performance. A number of applications only require read atomicity (RA) (either all or none of a transaction’s updates are visible to other transactions) and prevention of lost updates (PLU). Existing distributed transaction systems that meet these requirements also provide additional strong...... hiện toàn bộ
Process algebra with guards: Combining Hoare logic with process algebra
Formal Aspects of Computing - Tập 6 - Trang 115-164 - 1994
We extend process algebra with guards, comparable to the guards in guarded commands or conditions in common programming constructs such as ‘if — then — else — fi’ and ‘while — do — od’. The extended language is provided with an operational semantics based on transitions between pairs of a process and a (data-)state. The data-states are given by a data environment that also defines in which data-st...... hiện toàn bộ
Automatic verification of Java programs with dynamic framesAbstract
Framing in the presence of data abstraction is a challenging and important problem in the verification of object-oriented programs Leavens et al. (Formal Aspects Comput (FACS) 19:159–189, 2007). The dynamic frames approach is a promising solution to this problem. However, the approach is formalized in the context of an idealized logical framework... ... hiện toàn bộ
Formal Aspects of Computing - - 2010
Correctness and concurrent complexity of the Black-White Bakery AlgorithmAbstract
Lamport’s Bakery Algorithm (Commun ACM 17:453–455,
1974
) implements mutual exclusion for a fixed number of threads with the first-come first-served property. It has the disadvantage, however, that it uses integer communication variables that can become arbitrarily large.... ... hiện toàn bộ
Formal Aspects of Computing - Tập 28 Số 2 - Trang 325-341 - 2016
Compositional refinement in agent-based security protocols
Formal Aspects of Computing - Tập 23 - Trang 711-737 - 2010
A truly secure protocol is one which never violates its security requirements, no matter how bizarre the circumstances, provided those circumstances are within its terms of reference. Such cast-iron guarantees, as far as they are possible, require formal, rigorous techniques: proof or model-checking. Informally, they are difficult or impossible to achieve. Our rigorous technique is refinement, unt...... hiện toàn bộ
Functional specification and proof of correctness for time dependent behaviour of reactive systemsAbstract
A functional formalism for describing and reasoning about the time dependent behaviour of reactive systems is presented. The model is event based and can describe the histories of events with finite duration. It is a generalisation of the model of Caspi and Halbwachs (1986). A set of tools with their operations are introduced in the formalism and... ... hiện toàn bộ
Formal Aspects of Computing - Tập 3 Số 3 - Trang 253-283 - 1991
The Cash-Point Service in NUT
Formal Aspects of Computing - Tập 12 - Trang 222-224 - 2000
This paper describes how the cash-point service can be modelled and simulated using the NUT system.
Priority as extremal probability
Formal Aspects of Computing - Tập 8 - Trang 585-606 - 2015
We extend the stratified model of probabilistic processes to obtain a very general notion ofprocess priority. The main idea is to allow probability guards of value 0 to be associated with alternatives of a probabilistic summation expression. Such alternatives can be chosen only if the non-zero alternatives are precluded by contextual constraints. We refer to this model as one of “extremal probabil...... hiện toàn bộ
Tổng số: 714
- 1
- 2
- 3
- 4
- 5
- 6
- 10