Contact details: School of Computing, Information Systems and Mathematics,  London South Bank University, Centre for Applied Formal Methods Southwark Campus  103 Borough Road  London SE1 0AA  UK  Tel: +44 (0)20 7815 7025 Email: nissanke@sbu.ac.uk

	Realtime Systems Prentice Hall Series in Computer Science by Tony Hoare and Richard Bird. Prentice Hall, 1997. The book contains some material of considerable research interest. In addition to a comprehensive overview of real-time issues, the topics include a mathematical formulation of both ideal and real clocks, a precise relationship between clock time and real time, systems of clocks in the distributed multi-processor context, Petri nets as a modelling framework (ranging from basic concepts to timed nets and Environment-Relationship Nets), untimed and timed versions of Communicating Sequential Processes (CSP, due to Tony Hoare), software partitioning, task allocation, scheduling (covering uni-processor and multi-processor scheduling both statically and dynamically) and fault tolerance.
	Introductory Logic and Sets for Computer Scientists Addison Wesley Longman, 1999. The book is a gentle introduction to logic and set theory. Topics include propositional and predicate logic, sets, relations, functions, numbers from both mathematical and computational perspectives, Boolean algebra and lambda calculus.   Its features include simple explanations of concepts, plenty of examples, graded exercises and model answers. Its design pays particular attention to presentation so that the material is easily accessible to students with many different backgrounds.   For model answers, click here.
	Formal Specification - Techniques and Applications Springer-Verlag, 1999. The book covers formal specification in Z and VDM, specification of object oriented systems, specification of safety critical systems, algebraic specification. It pays particular attention to developing specification skills both with respect to abstraction and mathematical modelling of software.

Current Research

Probabilistic Approaches to Real-time Communications

Probabilistic Static and Dynamic Scheduling This work concentrates on the development of probabilistic approaches to  1) uni-processor static scheduling,  and  2) multi-processor scheduling in non-critical real-time applications.  A primary motivation for this work is its potential use in the provision of a required level of Quality of Service in real-time communications, particularly in the context of multimedia applications, over large packet-switched networks (e.g. the Internet, ATM). In this context, it is no longer meaningful to specify communication demands and available network resources in a deterministic manner due to unpredictability of traffic flow. In this connection, this research regards the probabilistic paradigm as a more appropriate framework for reasoning about issues such as admission control, routing, issuing service guarantees, etc., with a quantifiable measure of confidence.  Current research focuses on performance evaluation of multiprocessor scheduling environments, probabilistic priority driven uni-processor scheduling, probabilistic priority driven multi-processor scheduling, verification of probabilistic techniques using stochastic simulations, probabilistic techniques into jitter control.

Safety Critical Systems

Program Transformation for Safety Generic Safety Supervisor (GSS) is a concept of significant practical interest and aims at the identification of reusable safety critical software so that they can be better engineered and reused across different applications with minimal modifications. The GSS approach to making a system safe requires a deep understanding about what is meant by safety. In particular, it requires an understanding of what are failures, how do they arise, how do they propagate and how to contain their effects. In order to reason about these issues rigorously, a more fundamental study is required. In this respect, a formulation of a general mathematical framework in timed CSP is already under way. This framework addresses how to represent, and formally reason about, a variety of failures of different system components: equipment, sensors and the controller. These include timing failures (omission failures, temporal order failures, clock failures and crash) and logical failures (output failures, drift failures, Byzantine failures). The approach advocates a hierarchy of different abstractions. At the highest level of abstraction, items of equipment and the system are modelled in a way that each functions in an ideal manner. In subsequent stages, alongside a more detailed design, possible failure modes are incorporated into each item of equipment and sensors monitoring equipment, interfaces and the controller, but with little interest in their consequences. In the final stage, mechanisms are introduced to ensure safety. The work aims to show formally that in the absence of any failures the system behaves in the ideal manner but in the presence of failures it follows an expected pattern of safe behaviour.

Safecharts Safecharts is a variant of Statecharts – a visual formalism due to David Harel – and is intended exclusively for the design of safety critical systems. Strategy of Safecharts is to use Statecharts as used conventionally to represent functional requirements and to provide an extended notation to capture safety requirements. Safecharts distinguishes the use of the two notational devices, mentioned above, in terms of a functional layer and a safety layer and concentrates its effort exclusively on the features of the latter. Its unique approach to representation of functional and safety requirements helps both designers and auditors alike, by enabling, on the one hand, the designer to focus on safety issues with a clear understanding of how function affects safety and vice versa, and, on the other hand, the auditor to review safety critical requirements without being distracted by functional issues.  Among the features of the safety layer are the means to represent failures, an extended safety-oriented annotation of transitions and characterisation of states and, consequently, transitions according to risks posed by them. In respect of both layers, Safecharts shares in common the traditional virtues of Statecharts, namely, visual appeal, modular and hierarchical representation of systems and mathematical rigour.  A unique contribution of Safecharts is its approach to representation of risks. This is done explicitly by means of an ordering of states (referred to as a risk graph) according to risks posed by them and a supplementary concept of risk band. Recent research has extended the work to the study of interdependencies of risk at lower levels of abstraction (involving configuration states and node replacement in risk graphs). Another unique feature of Safecharts is the concept of situational event and the notion of dynamic risk graph which allows the modelling of changing circumstances of a safety critical system due to changes in the environment or, more importantly, due to a chain of unfolding failure, or repair, events.

Teaching

Real-time System at underground level This unit is based largely on the unit previously offered at University of Reading but has undergone substantial changes in its presentation in order to meet the needs of several undergraduate courses offered at South Bank University.

Mobile Computing at MSc level  This is a successor to two previous courses, one on Multimedia Information Systems and another on Distributed and Networked Multimedia, both introduced by me since 2000. The unit now covers a range of topics, including conventional wired communication infrastructures required to support multimedi applications, TCP/IP, mobile computer networks (Mobile IP, wireless networks, ad-hoc networks, personal area networks, Quality of Service), mobile computing applications (WAP and WML).

Commercial Networked Environments at MSc level This unit, introduced in 2003, concentrates on the design and development of enterprise-level web-centric applications based on multi-tier software architectures. It deals with issues such as the design of user interfaces, architectures to suit different business needs, systematic ways to modelling business logic, infrastructure facilities on transaction processing, security, etc., and system evaluation. It uses as J2EE as a development environment

A Selection of Scientific Papers

H. Dammag and N.Nissanke. A Mathematical Framework for Safecharts.  (to appear at ICFEM03, Singapore, 2003).

A. Leulseged and N. Nissanke.  Probabilistic Analysis of Multi-processor Scheduling of Tasks with Uncertain Parameters.  9th Int. Conf. On Real-time and Embedded Computing Systems and Applications, Taiwan, February 2003.

N.Nissanke and H. Dammag. Representation of Risk in Safecharts.  Journal of Safety Science. Elsevier, 40(9), December 2002. pp 753-763.

Nimal Nissanke, Amare Leulseged and Srinivas Chillara.  Probabilistic Performance Analysis in Multiprocessor Scheduling.  Computing and Control Journal, IEE, London, August, 2002.

L. David, F. Cottet and N. Nissanke.  Jitter Control in On-line Scheduling of Dependent Real-Time Tasks.  IEEE Real-time Systems Symposium, London, December, 2001.

Nimal Nissanke, Amare Leulseged and Srinivas Chillara. A Framework for Probabilistic Analysis of Multiprocessor Scheduling Environments.  IEEE/IEE Workshop on Embedded Real-time Systems, London, December, 2001

Nimal Nissanke. On a Probabilistic Approach to Fixed Priority Uni-Processor Scheduling of Repetitive Tasks.  IEEE Real-time Systems Symposium, Work in Progress, London, December, 2001

N.Nissanke and H.Dammag. Risk Ordering of States in Safecharts.  In Proceedings, 19th International Conference Computer Safety, Reliability and Security: SAFECOMP 2000. Rotterdam, Netherlands, October 2000. LNCS. Vol. 1943. SpringerVerlag.

N.Nissanke and H.Dammag.  Risk Bands - A Novel Feature of Safecharts. In Proceedings, 11th International Symposium on Software Reliability Engineering. 2000. San Jose, USA.

S. Veloudis and N. Nissanke. Modelling Coordinated Atomic Actions in Timed CSP.  In Proceedings, 6th International Symposium on Formal Techniques in Real-Time Fault Tolerant Systems: FTRTFT 2000.. Pune, India. September. 2000. LNCS 1926. SpringerVerlag.

H. Dammag and N. Nissanke. Safecharts for Specifying and Designing Safety Critical Systems. In Proceedings, 18th IEEE Symposium on Reliable Distributed Systems, Lausanne. October, 1999.

I. M. Smarandache and N. Nissanke. Applicability of SIGNAL in safety critical system development.  IEE Proceedings: Software, IEE, UK, 146(2): 86-95, April, 1999.

S. Veloudis and N. Nissanke. Duration calculus in the specification of safety requirements. Formal Techniques in Real-Time and Fault-Tolerant Systems, LNCS 1486, pages 103-112. Springer-Verlag, September 1998.

N. Nissanke. Safety specification in deontic logic. In Proceedings, 2nd IMA Conference on the Mathematics of Dependable Systems, York, England, pages 113-133. Oxford University Press, 1997.

J. P. Thomas and N. Nissanke. An algebra for modelling assembly tasks. Mathematics and Computers in Simulation, IMACS journal, 41:640-659, 1996.

J. P. Thomas, N. Nissanke, and K. D. Baker. Boundary models for assembly knowledge representation. IEEE Transactions on Robotics and Automation, 12(2): 302-312, April 1996.

J. P. Thomas, N. Nissanke, and K. D. Baker. A hierarchical Petri net framework for the representation and analysis of assembly.  IEEE Transactions on Robotics and Automation, 12(2): 268-279, April 1996.

N Nissanke.  An approach to specification of realtime systems.  Proceedings, 20th IFAC/IFIP Workshop on Real-time Programming, pages 51-58. Elsevier Press, 1996.

N Nissanke and R. J. Loader.  Reactive scheduler for realtime systems. In  Proceedings, 20th IFAC/IFIP Workshop on Real-time Programming, pages 107-114. Elsevier Press, 1996.

J. P. Thomas and N. Nissanke. A decomposition approach for performance evaluation of non-pipelined systems. In Proceedings, INRIA/IEEE Conf. on Emerging Technologies and Factory Automation, Paris, France, pages 195-206, Aug 1995.

J. P. Thomas and N. Nissanke. A graph-based formalism for modelling assembly tasks. In Proceedings, IEEE Int. Conf. on Robotics and Automation, Nagoya, Japan, pages 1296-1301, 1995.

J. P. Thomas and N. Nissanke.  A model for throughput evaluation in manufacturing systems. In Proceedings, INRIA/IEEE Conf. on Emerging Technologies and Factory Automation, Paris, France, pages 323-334, Oct 1995.

J. P. Thomas and N. Nissanke. Properties of assembly Petri net. In  Proceedings, IEEE Int. Conf. on Intelligent Robots and Systems, Pittsburgh, PA, Aug 1995.

N. Nissanke and J. P. Thomas. A formal framework for design. In J. S. Gero and F Sudweeks, editors,  Advances in Formal Design Methods for CAD, IFIP WG5.2 Second Workshop in Formal Design methods for CAD, Mexico City, pages 349-369, 1995.

N. Nissanke. Towards refinement in programming realtime systems. In Proceedings, 7th Euromicro Workshop on Real Time Systems, pages 244-251. IEEE Computer Society, June 1995.

J. P. Thomas and N. Nissanke.  An algebra for modelling assembly tasks. In Proceedings, European Robotics and Intelligent Systems Conference, Malaga, Spain, pages 436-455, 1994.

N. Nissanke and N. Robinson. Formal methods in safety analysis. In V. Maggioli, editor, SAFECOMP'94, International Conference on Computer Safety, Reliability and Security, pages 239-248, Anaheim, California, 1994. Instrument Society of America.