© 1996-2021

| | | ||

| ## 3.2 FLCheck: Fusion Logic decision ProcedureFusion Logic augments conventional Propositional Temporal Logic (PTL) with the fusion operator. Note: the fusion-operator is basically a “chop” that does not have an explicit negation on the left hand (for right fusion logic) side (as fusion expression) or the right hand (for left fusion logic). The negation is implicit, i.e., the negation is a derived fusion expression operator. The expressiveness of Fusion Logic is the same as Propositional Interval Temporal Logic. The main diﬀerences concern computational complexity, naturalness of expression for analytical purposes, and succinctness. Fusion Logic is closely related to Propositional Dynamic Logic (PDL). We have implemented above decision procedure for Fusion Logic in Tcl/Tk and the CUDD BDD library. The tool allows one to check the validity or satisﬁability of a Fusion Logic formula. If a formula is not valid it will produce a counter example and if a formula is satisﬁable it will produce an example model. Figure 4 gives a screen dump of our tool which is available at - FLCHECK version 1.2 (released 22/05/2015).
Main Changes: - Added support for MacOSX.
- Added pre-compiled binary for MacOSX.
- FLCHECK version 1.1 (released 04/07/2013).
Main Changes: - Drop support for Solaris Sparc.
- Added pre-compiled binaries for Windows (XP and 7) and Linux (Ubuntu 12.04, 32 and 64 bits).
- FLCHECK version 1.0 (released 23/01/2013).
Main Changes: - Simpliﬁed ‘left always followed by’ operator.
- Added more examples.
- FLCHECK version 0.9 (released 21/02/2012).
Main Changes: - Introduction of left and right Fusion Logic which makes the speciﬁcation of access control policies much simpler
- Use of time reversal to rewrite left fusion logic formulae into right fusion logic formulae
- Enforcement of policies expressed in left Fusion Logic
- All examples come now with comments
- FLCHECK version 0.8 (released 26/03/2010).
Initial release.
- Antonio Cau, Helge Janicke, and Ben Moszkowski. Veriﬁcation and enforcement of access control policies. Formal Methods in System Design, Springer, 2013.
- A Note on Expressing Policy Rules in Fusion Logic, A. Cau. Technical report, STRL, De Montfort University.
| | ||

| |