Search

Dynamic logic and its variations, because of their clear and expressive forms for capturing program properties, have been used as formalisms in program/system specification and verification for years and have many other applications. The program models of dynamic logics are in explicit forms. For different target program models, different dynamic logic theories have to be proposed to adapt different models' semantics. In this paper, we propose a parameterized `dynamic-logic-style' formalism, namely $DL_p$, for specifying and reasoning about general program models. In $DL_p$, program models and logical formulas are taken as `parameters', allowing arbitrary forms according to different interested domains. This characteristic allows $DL_p$ to support direct reasoning based on the operational semantics of program models, while still preserving compositional reasoning based on syntactic structures. $DL_p$ provides a flexible verification framework to encompass different dynamic logic theories. In addition, it also facilitates reasoning about program models whose semantics is not compositional, examples are neural networks, automata-based models, synchronous programming languages, etc. We mainly focus on building the theory of $DL_p$, including defining its syntax and semantics, building a proof system and constructing a cyclic preproof structure. We analyze and prove the soundness of $DL_p$. Case studies show how $DL_p$ works for reasoning about different types of program models., Comment: Minor modifications from the last version

We analyze a phenomenon called ``image reflection'' on a type of characterization graphs -- LLEE charts -- of 1-free regular expressions. Due to the correspondence between 1-free regular expressions and the provable solutions of LEE/LLEE charts, this observation naturally leads to a new proof for the completeness of the proof system \MilIfree\ for 1-free regular expressions modulo bisimulation equivalence. The critical part of the previous proof is to show that bisimulation collapse, which plays the role in linking the provable solutions of two LLEE charts, is still an LLEE chart. The difference of our proof, compared to the previous one, is that we do not rely on the graph transformations from LLEE charts into their bisimulation collapses by merging two carefully-selected bisimilar nodes in each transformation step. Instead, we directly show that the bisimulation collapse of an LLEE chart possesses an LEE/LLEE structure based on its set of images mapped through the bisimulation function from the LLEE chart, and the constrained relation between the images and their so-called ``well-structured'' looping-back charts pre-images on the LLEE chart. Our approach provides a novel angle to look at this problem and related problems, and can also be used for simplifying the graph transformations in the proof of the completeness problem of the proof system \Mil\ for regular expressions modulo bisimulation equivalence, which had remained open until very recently., Comment: Minor typos and further polishing from the reviewers' comments of the conference that rejected us

Synchronous model is a type of formal models for modelling and specifying reactive systems. It has a great advantage over other real-time models that its modelling paradigm supports a deterministic concurrent behaviour of systems. Various approaches have been utilized for verification of synchronous models based on different techniques, such as model checking, SAT/SMT sovling, term rewriting, type inference and so on. In this paper, we propose a verification approach for synchronous models based on compositional reasoning and term rewriting. Specifically, we initially propose a variation of dynamic logic, called synchronous dynamic logic (SDL). SDL extends the regular program model of first-order dynamic logic (FODL) with necessary primitives to capture the notion of synchrony and synchronous communication between parallel programs, and enriches FODL formulas with temporal dynamic logical formulas to specify safety properties -- a type of properties mainly concerned in reactive systems. To rightly capture the synchronous communications, we define a constructive semantics for the program model of SDL. We build a sound and relatively complete proof system for SDL. Compared to previous verification approaches, SDL provides a divide and conquer way to analyze and verify synchronous models based on compositional reasoning of the syntactic structure of the programs of SDL. To illustrate the usefulness of SDL, we apply SDL to specify and verify a small example in the synchronous model SyncChart, which shows the potential of SDL to be used in practice.

This thesis focuses on the wireless security in the physical layer with beamforming technique. One of the emerging areas is the security enhancement in the physical layer, which exploits the intrinsic properties of the wireless medium. Beamforming, which has been proved to have many advantages, can also be applied to enhance the wireless security. One of the most common threats, i.e., passive eavesdropping, is addressed in this thesis. To reduce the risk of leaking information to the eavesdroppers, the physical region where the transmission is exposed to eavesdropping has been studied. In this thesis, the exposure region based beamforming technique is proposed to combat the threat from the randomly located eavesdroppers in a fading channel. In this system model, the large-scale path loss and a general Rician fading channel model are considered. The exposure region is established to describe the secrecy performance of the system, based on which the probability that the secrecy outage event occurs is defined to evaluate the security level of the exposure region. The antenna array is one of the most important factors that affect the secrecy performance of the exposure region based beamforming technique. The potential of using different array geometry and array configuration to improve security is explored. In this thesis, two common arrays, i.e., linear and circular arrays, are considered.Analytic expressions for general array geometry and for the linear and circular arrays are derived. Based on the empirical results, numerical optimization algorithms are developed to exploit the array configuration to enhance the system security level. In addition, experiments are carried out to study the performance of the beamformer with linear and circular arrays. Especially, the impact of the mutual coupling on the security performance is investigated., Comment: 237 pages; PhD thesis

With increasing number of antennae in base stations, there is considerable interest in using beamfomining to improve physical layer security, by creating an `exposure region' that enhances the received signal quality for a legitimate user and reduces the possibility of leaking information to a randomly located passive eavesdropper. The paper formalises this concept by proposing a novel definition for the security level of such a legitimate transmission, called the `Spatial Secrecy Outage Probability' (SSOP). By performing a theoretical and numerical analysis, it is shown how the antenna array parameters can affect the SSOP and its analytic upper bound. Whilst this approach may be applied to any array type and any fading channel model, it is shown here how the security performance of a uniform linear array varies in a Rician fading channel by examining the analytic SSOP upper bound., Comment: Submitted to the IEEE Transactions on Wireless Communications