Dr Francois Siewe

Job: Reader in Computer Science

Faculty: Computing, Engineering and Media

School/department: School of Computer Science and Informatics

Research group(s): Cyber Technology Institute (CTI) (Software Technology Research Laboratory (STRL))

Address: 冈本视频, The Gateway, Leicester, LE1 9BH, United Kingdom

T: +44 (0)116 257 7938

E: FSiewe@dmu.ac.uk

Close all sections

Open all sections

Personal profile

I am a Reader in Computer Science in the Software Technology Research Laboratory (STRL) of the Faculty of Technology at 冈本视频 (冈本视频), in Leicester in the UK. Before joining STRL, I was a research fellow on the EPSRC-funded project MELANGE on modelling the structure dependent colour properties of melange yarns in the Textile Engineering And Material (TEAM) research group at 冈本视频. This followed my tenure as lecturer and vistiting researcher in the Institute of Technology of Lens at University of Artois in Lens, France. Prior to this, I was a fellow at the United Nation University/ International Institute for Software Technology (UNU/IIST) in Macau, where I worked on the Design Techniques for Reat-time systems (DeTfoRs) project. I was also a lecturer in the Department of Mathematics and Computer Science at the University of Dschang, Dschang, Cameroon.

Research group affiliations

Software Technology Research Laboratory (STRL)

Publications and outputs

dc.title: Towards a Formal Verification of IoT System Models Designed in the Cisco Packet Tracer Tool dc.contributor.author: Siewe, Francois dc.description.abstract: The Cisco Packet Tracer (CPT) is a network and IoT systems design and simulation tool developed by Cisco Systems inc. The tool is widely used in academia and the industry to develop and simulate complex IoT systems for training purposes. Although the graphical notations of CPT are appealing to system developers, the tool does not support formal verification. Therefore, CPT is limited when it comes to the design and development of safety and secutiry critical IoT systems where faults can endanger people鈥檚 lives or damage properties and businesses. This paper proposes a formal approach to the verification of IoT system models designed in the CPT tool, based on the Calculus of Context-aware Ambients (CCA). First, the graphical notations of CPT are mapped to processes in CCA that specify their behaviours. Then any desired property of a system can be specified as a Linear Temporal Logic (LTL) formula. Finally, the CCA Runtime Verification tool ccaRV is used to verify formally whether the behaviour of an IoT system model designed in CPT violates the system鈥檚 requirements. The pragmatics of the proposed approach is illustrated using a case study.
dc.title: Runtime Verification Tool for the Calculus of Context-Aware Ambients dc.contributor.author: Siewe, Francois dc.description.abstract: A context-aware system is a system that adapts its behaviours in response to changes in the system鈥檚 environment (i.e., context). Ensuring the correctness of such a system is difficult because the state of the environment changes frequently in an unpredictable manner according to the laws of physics. Hence, formal verification techniques like model-checking and theorem proving do not work in many cases. Runtime Verification (RV) is a lightweight formal verification technique that consists of checking at runtime whether the execution of the system violates the requirements of the system. The Calculus of Context-aware Ambients (CCA) is a process calculus for modelling context-aware systems and reasoning about their behaviours. This paper proposes an RV tool for CCA, called ccaRV. Given a model of a system in CCA and a property of the system written in LTL (Linear Temporal Logic), ccaRV verifies automatically at runtime if the execution of the system violates the property. We propose a semantic approach to RV, where the RV mechanism is defined at the semantics level and not as an add-on. A consequence of this is that there is no need for generating a monitor from the property specification nor for the instrumentation of a system during verification. We define a labelled reduction relation for CCA, where the labels are used to capture the execution traces at the semantics level. Then we extend LTL with spatial operators and context expressions in order to formulate properties about the system context. We use a case study of the MQTT (Message Queue Telemetry Transport) protocol to evaluate the proposed RV approach. The results show that the ccaRV tool is scalable and its decisions are accurate. dc.description: open access article
dc.title: A Compositional Framework for the Development of Secure Access Control Systems dc.contributor.author: Siewe, Francois dc.description.abstract: Security requirements deal with the protection of assets against unauthorised access (disclosure or modification) and their availability to authorised users. Traditionally, security concerns are considered as an add-on to be implemented at a later stage of system development. Nowadays, it is well understood that adopting such belief can be difficult and error-prone. Therefore security must be considered as an integral part of the system requirements right from the early stages of the system development life cycle. In this thesis, we develop a unified compositional formal framework for the specification of the functional, temporal and security requirements of systems. The framework uses a single formalism. Interval Temporal Logic (ITL in short), for expressing the three types of requirements and for reasoning about them in a uniform manner. This provides an effective way of integrating security concerns into the system requirements and to address them early (high level specifications) in the system development process so that security holes can be detected and fixed timely. We propose a language for expressing access control policies and their composition. Especially, a set of operators is defined for expressing policies that can change dynamically in response to time or events. The resulting model provides a high flexibility to support the specification of several protection requirements that cannot be expressed in traditional access control models. We investigate the algebraic properties of the operators and develop sound algebraic laws for the comparison and the refinement of security policies. We take the view that a system is developed starting from a high level specification and transformed by a sequence of correctness preserving refinement steps down to a low level implementation. The low' level system must implement a mechanism for enforcing security policies. In this respect, we develop a computational model. Secure Action System (SAS), that allows the enforcement of dynamically changing security policies. It is an extension of the traditional action system paradigm to cater for security. SASs can be composed into a large system. We propose a rich set of sound compositional rules for the design and verification of SASs. We develop a tool, SPAT, to animate security policy specifications and to analyse them. We evaluate our approach with a detailed case-study of a secure exam system and the formalisation of the British Medical Association鈥檚 security policy for Electronic Patient Records (EPRs).
dc.title: Predicting Illnesses from Medical Sensors Readings using Artificial Intelligence Model dc.contributor.author: Siewe, Francois; Germanos, Vasileios; Zeng, Wen; Jawad, H. A.; Wang, W.; Molina鈥揓imenez, C. dc.description.abstract: The cost and lack of flexibility of health care systems represent a major obstacle for the elderly and poor citizens. The current technologies are reserved for hospitals and large clinics in the developed countries have high costs and maintenance. Therefore, it is necessary to bring health monitoring closer to the patients and healthcare providers in a cost-effective way. This study aims to build a platform that is ready to expand to use all the sensors to predict illnesses and conditions in hospitals and homes. The system is based on two Arduino Uno microcontroller units (MCU), environmental sensors, health sensors (MySignals), and Arduino IDE. Fuzzy Logic is used to push and pull data from the cloud to mobile and web visualization plus an alert system. This study tested 15 sensors in both health and ambient environments the integration of both groups of sensors can produce more accurate predictions. In addition, metrics will be used to decide the range of readings that are industry-specific for each sensor.
dc.title: A Business Plan for Data Security and Privacy Services dc.contributor.author: Germanos, Vasileios; Zeng, Wen; Smith, Abigail; Carroll-Mayer, Moira; Siewe, Francois dc.description.abstract: Cyber Security Academic Startup Programme (Cyber Asap) provides academics with the expertise, knowledge and training needed to convert their research into technologies, products and services. Due to the fast development of digital technologies, data security and privacy became an active research topic. However, we do not have business plan templates for data security and privacy. Therefore, it is necessary to develop a business plan for data security and privacy technologies, which can help the data security and privacy research out of the university lab and into the commercial market. In this study, technical and non-technical risks and related contingency plans will be addressed through consideration of risk management and secure system architecture.
dc.title: On the Execution and Runtime Verification of UML Activity Diagrams dc.contributor.author: Siewe, Francois; Ngounou, Guy Merlin dc.description.abstract: The unified modelling language (UML) is an industrial de facto standard for system modelling. It consists of a set of graphical notations (also known as diagrams) and has been used widely in many industrial applications. Although the graphical nature of UML is appealing to system developers, the official documentation of UML does not provide formal semantics for UML diagrams. This makes UML unsuitable for formal verification and, therefore, limited when it comes to the development of safety/security-critical systems where faults can cause damage to people, properties, or the environment. The UML activity diagram is an important UML graphical notation, which is effective in modelling the dynamic aspects of a system. This paper proposes a formal semantics for UML activity diagrams based on the calculus of context-aware ambients (CCA). An algorithm (semantic function) is proposed that maps any activity diagram onto a process in CCA, which describes the behaviours of the UML activity diagram. This process can then be executed and formally verified using the CCA simulation tool ccaPL and the CCA runtime verification tool ccaRV. Hence, design flaws can be detected and fixed early during the system development lifecycle. The pragmatics of the proposed approach are demonstrated using a case study in e-commerce. dc.description: open access article
dc.title: Mapping Petri Nets onto a Calculus of Context-Aware Ambients dc.contributor.author: Siewe, Francois; Germanos, Vasileios; Zeng, Wen dc.description.abstract: Petri nets are a graphical notation for describing a class of discrete event dynamic systems whose behaviours are characterised by concurrency, synchronisation, mutual exclusion and conflict. They have been used over the years for the modelling of various distributed systems applications. With the advent of pervasive systems and the Internet of Things, the Calculus of Context-aware Ambients (CCA) has emerged as a suitable formal notation for analysing the behaviours of these systems. In this paper, we are interested in comparing the expressive power of Petri nets to that of CCA. That is, can the class of systems represented by Petri nets be modelled in CCA? To answer this question, an algorithm is proposed that maps any Petri net onto a CCA process. We prove that a Petri net and its corresponding CCA process are behavioural equivalent. It follows that CCA is at least as expressive as Petri nets, i.e., any system that can be specified in Petri nets can also be specified in CCA. Moreover, tools developed for CCA can also be used to analyse the behaviours of Petri nets. dc.description: open access article
dc.title: Forest Fire Detection Utilizing Ghost Swin Transformer with Attention and Auxiliary Geometric Loss dc.contributor.author: Siewe, Francois; Wang, Lili; Li, Haiyan; Ming, Wenjun; Li, Hongsong dc.description.abstract: Forest fires are a devastating natural disaster. Existing fire detection models face limitations in dataset availability, multi-scale feature extraction, and locating obscured or small flames and smoke. To address these issues, we develop a dataset containing real and synthetic forest fire images, sourced from a UAV (Unmanned Aerial Vehicle) perspective. Additionally, we propose the Ghost Convolution Swin Transformer (GCST) module to extract multi-scale flame and smoke features from different receptive fields by integrating parallel Ghost convolution and Swin Transformer. Subsequently, we design a lightweight reparameterized rotation attention module, which captures interactions across channel and spatial dimensions to suppress background noise and focus on obscured flames and smoke. Finally, we introduce a loss function, called Efficient Auxiliary Geometric Intersection over Union (EAGIoU), which employs an auxiliary bounding box to accelerate the model's convergence while integrating the geometrical principles of the predicted and real bounding boxes to accurately locate small flames and smoke. Extensive experimental results demonstrate that our method achieves 75.2% mAP@0.5 and 42% mAP@0.5:0.95 with a frame rate of 239 frames per second, indicating a significant improvement in accuracy and real-time performance compared to state-of-the-art techniques. The code and datasets are available at https://github.com/luckylil/forest-fire-detection. dc.description: The file attached to this record is the author's final peer reviewed version. The Publisher's final version can be found by following the DOI link.
dc.title: Practical Consequences of Quality Views in Assessing Software Quality dc.contributor.author: Galli, Tamas; Chiclana, Francisco; Siewe, Francois dc.description.abstract: The authors鈥� previously published research delved into the theory of software product quality modelling, model views, concepts, and terminologies. They also analysed this specific field from the point of view of uncertainty, and possible descriptions based on fuzzy set theory and fuzzy logic. Laying a theoretical foundation was necessary; however, software professionals need a more tangible and practical approach for their everyday work. Consequently, the authors devote this paper to filling in this gap; it aims to illustrate how to interpret and utilise the previous findings, including the established taxonomy of the software product quality models. The developed fuzzy model鈥檚 simplification is also presented with a Generalized Additive Model approximation. The paper does not require any formal knowledge of uncertainty computations and reasoning under uncertainty, nor does it need a deep understanding of quality modelling in terms of terminology, concepts, and meta-models, which were necessary to prepare the taxonomy and relevance ranking. The paper investigates how to determine the validity of statements based on a given software product quality model; moreover, it considers how to tailor and adjust quality models to the particular project鈥檚 needs. The paper also describes how to apply different software product quality models for different quality views to take advantage of the automation potential offered for the measurement and assessment of source code quality. Furthermore, frequent pitfalls are illustrated with their corresponding resolutions, including an unmeasured quality property that is found to be important and needs to be included in the measurement and assessment process. dc.description: open access article
dc.title: Towards the Formal Analysis of UML Activity Diagrams in a Calculus of Context-aware Ambients dc.contributor.author: Siewe, Francois dc.description.abstract: The Unified Modeling Language (UML) is the industrial de-facto standard for designing systems. It has been used widely in many industrial applications. However, the lack of formal semantics for UML makes it unsuitable for formal verification. As such, UML is limited when it comes to the design of safety/security critical systems where faults can cause damages to people, properties, or the environment. This paper proposes an attempt to define a formal semantics for the UML activity diagrams. An algorithm is proposed that translates an activity diagram into a process in a Calculus of Context-aware Ambients (CCA). This process can then be formally analysed using the tool support for CCA. Hence, errors can be detected and fixed early during the system development life-cycle. The pragmatics of the proposed approach is demonstrated using a case study in e-commerce. dc.description: The file attached to this record is the author's final peer reviewed version. The Publisher's final version can be found by following the DOI link.

Research interests/expertise

Computer Security

Pervasive Systems

Formal Methods

Process Calculi

Formal Verification

Qualifications

PhD in Computer Science, 冈本视频, Leicester, UK, 2005

Doctorat de Troisième Cycle, Université de Yaoundé I, Yaoundé, Cameroon, 1997

Msc in Computer Science, Université de Yaoundé I, Yaoundé, Cameroon, 1992

Bsc in Maths & Computer Science, Université de Yaoundé, Yaoundé, Cameroon, 1990

冈本视频 taught

Pervasive Systems

Honours and awards

Research Journal of Textile and Apparel (RJTA) Excellent Paper Award 2011

Current research students

First supervisor for:

Ahmed Mohammed Alalshuhai
Abdulgader Zaid Almutairi
Saud Maqed Almutairi
Muslit Awadh Alotaibi
Asma Abdulghani Qasem Al-Shargabi
Elena Chernikova
Abdulghani Mahmoud Suwan

Second supervisor for:

Abdullah Shawan Alotaibi
Amr Mohsen Jadi