[:en]The feasibility of the proposal concerns the establishment TEI workshop in Crete which promotes scientific research in important fields such as Artificial Intelligence and Software Engineering and particularly in areas such as Programming Logic, Methodology and Design in Network Systems and Chip, and medical applications in cooperation with known international universities, research centers and companies. The activities of this sub-project are abovementioned areas. We hope that this sub-project will help develop research, especially in the presence of better research, the establishment and improvement of the existing laboratory infrastructure “Artificial Intelligence and Software Engineering” of the TEI of Crete. Also the cooperation with leading universities and companies in particular, we think that will make its Applied Technology Research in the Technological Educational Institute of Crete.

 

Activity 1: Tools for Transformation and Verification Programs

The software development is an activity that often begins in an informal and vague claim of what needs to be done and results in a very detailed standard object system software. The software development process requires much work, but it is prone to mistakes. Moreover, the final result does not contain the design knowledge which led to the construction of software system. This design knowledge needs to be maintained and updated to reused to develop new software systems.

There are software development methodologies that produce very structured programs [Marakakis94, Marakakis97]. Production programs reflect the design decisions that have followed in its construction. These methods produce an executable program draft despite an effective program. A effectiveness is not an issue that should be taken into account during the construction phase of the program. The advantages of such methodologies are: 1) The program manufactured by the very structured form can be used for maintenance of the program and proof of program properties. Changes in the program may be made at the level of design decisions. That is, change in the mean change in a set of design decisions. 2) Proof of correctness of the manufactured programs facilitated by the highly structured form. 3) A tool can be constructed which will automatically transform the structured programs in relevant and more effective smaller, which will be used for running.

This sub-project aims to develop tools using Artificial Intelligence techniques that will enhance and demonstrate the validity of such methods of construction software [Marakakis94, Marakakis97]. Furthermore, we studied the fields of transformation programs and the verification program. We aim to develop the following tools: 1) Construction of an automatic or semi-automatic tool which will transform the very structured programs in relevant more compact (less code) and more effective programs. 2) Develop an interactive verifiers (verifier) o which proves the correctness of the manufactured programs. Furthermore, we studied the relationship which can be manufactured in the structure of programs and structure of the proof of correctness.

The software will be built and the method of logical construction of programs [Marakakis94, Marakakis97] will be used in courses on software development (Programming / tion II, Software Technology). In addition, we implemented advanced techniques of Artificial Intelligence. These will be used in classroom teaching Artificial Intelligence. We aim to get in contact with companies developing software that will use more of ‘results of this activity.

 

1.1. Transforming logic programs more effectively and respectively smaller.

The first work to transform programs in software development in anafererai article Burstall and Darlington [Burstall-Darlington77]. In its most general form of a transformation is a relationship between two shapes S and T programs. The transformation is considered correct if a valid semantic relation between S and S ‘[Partsch-Steinbruggen83]. The most important relationship is semantic equivalence.

The first transformation system for programs without reasonable refusal based on growth transformations (fold) – development (unfold), developed by Tamaki and Sato [Tamaki-Sato84]. Article [Shepherdson92] is extending the effects of Tamaki and Sato in regular programs where reasonably negative elementary formulas (literals) are allowed in the body of the proposals. Improving efficiency is not guaranteed when the transformation rules applied undisciplined, without any particular order. That is why the strategic changes introduced by Pettorossi and Proietti [Pettorossi-Proietti96], [Pettorossi-Proietti02]. Strategic changes are meta-rules that guide the application of transformation rules imposing the following rules apply katalilon transformation so as to improve the effectiveness of the programs produced.

The goal of transformation programs to improve efficiency while preserving the semantics of the program. The transformation starts from an initial plan, P0, and after one or more elementary transformations rules apply. Thus, we take a sequence P0, .., HN programs. We want the final program HN have the same semantics as the corresponding initial P0. This is achieved if efarmosome transformation rules which preserve the semantics. So, for two programs P semantics (P) = semantics (P) is valid if P can be produced by applying a single transformation rule [Pettorossi-Proietti96], [Pettorossi-Proietti02]. We usually want the RL to be more effective than P0. We also consider the following transformation rules for logic programs. 1) a new rule definition. 2) Standard Development (unfold). 3) Rule Development (fold). 4) Standard replacement target. 5) Rule deletion proposal.

The ineffectiveness of the programs produced by the method [Marakakis94, Marakakis97] may be due to a very structured form. The ineffectiveness of these programs can be corrected by applying logical rules of transformation programs as those mentioned above. The aim of these transformations is to remove programs from the design level with their size decreases and to do more effectively.

 

1.2. Verifier Logical Programs

There are two approaches to the problem of correctness of a program. The approach includes an examination of the program with a finite set of controls. The tests can show that a program has no errors for a given finite set of controls. For programs with complex input / output is difficult to show the correctness or not. Consideration of a program may not show complete absence of errors. The other approach is to prove that a program is correct with respect to the requirements of formal reasoning.

Considering that the program is a specification given there are two main approaches to the proof of correctness. In the first approach, accuracy is ensured by the construction of [Deville90, Flener00, Hogger81, Morgan90]. In this case a specification is improved sequentially in a program. The fabrication process is either smaller than pre-development steps whose correctness has been proved or transformations which preserve equivalence, ie transforming a specification or an equivalent program in another form. In the second approach, a program first constructed with a methodology and then demonstrate the correctness in relation to the specification of [Bossi-Cocco89, Clark80].

The first order logic (LPT) is a formalism used for specification of programs in procedural, logical and Functional Programming. The boundaries between specifications and programs are not strictly in logical programming languages. The advantage in comparison with the procedural programming languages is the proximity to the first order logic. Using the same formalism for specification and for facilitating the verification of programs and program production standards.

In literature there are several approaches to verify programs that use the LPT as the language specification [Clark80, Dayantis87, Deville90, Hansson-Tarnlund79, Tarnlund79]. In these approaches a specification consists of a set of types of LPT. Each specification type is a relationship which can be expressed according to other relations to the level of key components. A formal specification is called the LPT logic specification.

Types (types) is an important part of the specification. The nature of knowledge involved in specification formulas. Specifications are based in logic and no types are not sufficiently expressive for specification of large software systems. Popular languages specifications designed for specification of complex software systems using logic with types [Jones90, Spivey92].

A logical specification in our approach essentially follows the approaches based on LPT LPT uses but with types and gender. We aim to develop a semi-automatic verifier proof of logical correctness of programs which are manufactured by the method [Marakakis94, Marakakis97] in relation to the standards expressed in LPT with formulas. The verifier will be guided by the programmer. That is, the programmer selects exports conclusions (inferences) and the verifier will perform. We see such a verifier to be more automatic proof decisions gradually moving from the developer to the system. The verifier can prove lemmas which can then be used in subsequent proofs. The verifier drawn from outside the first class will be able to perform and inductive proof.

Activity 2: Certification systems and networks on chip

To find errors, complex systems, such as system or network chip to chip (system-on-chip, network on-chip), usually held two controls:

– Verify (verification). By verifying the check that grow well in accordance with the specifications. The verification takes place when there is a finished part that is working normally and usually following the control cycle model software (software cycle model).

– Certification (validation): The certification states that the system developed is what the customer and end user wish. The certification for each use case, usually using simulation (simulation) to examine the interactions with the system. This sends or receives messages to / from the information system or switches the system to control the initialization of each subsystem, to examine the temporal flow of messages (events, messages) as alternative flow of events, and check the equivalence of for each intended use

There are many open problems related to the activities of verification and certification systems on chip or in chip networks

  •  Existing models subsystems (software) are often developed and tested with different tools, resulting in a heterogeneous environment. Thus only the compatibility (interoperability) complex and different tools and languages can provide opportunities for reuse (software reuse).
  •  Modeling of system that can coexist at different levels of abstraction (abstraction levels) require separate verification and certification.
  •  The modeling system requires efficient parallel or distributed simulation.
  •  Existing tools for verification (in the system or block) is dependent on the implementation, it is not easy to change parameters without architectural xanaschediastei start the verification environment.

 

The first generation of tools for automatic verification methods based on modeling temporal logic (temporal logic). The system (circuit or process) is described as a finite machine situations (finite state machine), while the properties expressed as temporal logic formulas to express potential interrelationship (mutual exclusion), simultaneous access, and justice (fairness). One example is the SMV developed Carnegie Mellon University and uses computer logic tree (Computational Tree Logic, or CTL) [Clarke-Grumberg94]. This technique has been used successfully, eg to verify systems like Futurebus bus and PCI local bus.

Some properties are not expressed in CTL, but may be expressed as a finite (and vice versa). Thus a second approach uses the method of sub-languages (language containment) to check that the properties of the system expressed as a finite automatically contain the necessary contact. The system COSPAN, was developed experimentally by Bell Labs, and is now used tools from Cadence [Krurshan94]. We also note that the HSIS system developed Univ. Berkeley uses a combination of both techniques [Brayton94, Brayton-Hachtel96].

Most errors are discovered during the simulation could have been discovered sooner, at less cost with technical analysis and simulation high level. We will consider a user-friendly, environmental certification, designing and implementing a parallel or distributed tool for static and dynamic analysis capabilities provide verification system properties with the base user requirements. This tool, based on graph theory and methods of combination (combinatorics), could also be confirmed in real-time compound, possibly asynchronous system models using feasible schedules (reachability matrices), or with estimates of reliability (reliability).

In particular, the technical issues to be studied include techniques for simultaneous access (concurrency) and recovery (recovery) for the design of advanced parallel and distributed data structures and algorithms [Narayan-etal96]. We rely on graph theory (graph theory), the combination (combinatorics), the likelihood (probabilistic algorithms), and artificial intelligence techniques that can be used to represent constraints and certification systems or networks on chip. In particular, we will use the object-based modeling systems with the new industry standard SystemC2.0 [www-systemc]. The main open source software to be used initially consist of new verification tools and simulation systems to chip, eg o Testbuilder of Cadence, the standard SCV (SystemC Verification Library) [www-systemc], and recent articles which refer to the specific general technical certification system, as shown below

. The programming environment will be used and implemented in the respective optional subjects TEI to be a combination of valuation / imaginative techniques (combinatorics, heuristics) and to improve the efficiency of the system with new efficient algorithms. Also hoping for cooperation with industry for the proper use of.

 

Activity 3: Information Support System for Diagnosis of Childhood Epilepsy

 

3.1 A review of research

During the last thirty years have been significant research efforts to develop methods capable of dealing with complex problems such as those related to medical diagnosis.

The first comprehensive book which refers to the technical development of systems supporting medical diagnosis, written by Szolovits and published in 1982 under the title “Artificial Intelligence in Medicine” [Szolovits82]. This version, made extensive reference to the first diagnostic support systems, presenting the methodologies that were developed by then and was the starting point for research in this area the decade that followed.

Certainly in some way each system that has to do with management of some medical data or the reproduction of medical knowledge can be considered to contribute to clinical diagnosis. So Shortliffe [Shortliffe87] states that there are three basic types of systems, which can provide assistance in the process of diagnosis:

  1. Systems that do simple data management.
  2. Systems are designed to attract the attention of the user at certain points during the diagnosis.
  3. Advisory systems which are based on information relating to specific patients (patient-specific).

In 1994 the Miller [Miller94] presents an extensive study on the evolution of systems supporting medical diagnosis. In this survey indicated that almost all the efforts of researchers by then, demonstrating the importance of this sector. At the end of this article the author concludes by predicting that the future of medical decision support systems (MDDS) long deleted and that the number of researchers in this field will grow. Sees no significant commercial interest from companies in the area for such systems and that as they advanced information technology will become increasingly attractive for clinical data management for an effective health care.

Shortly thereafter, the M Reedman a relevant article [Reisman96] distinguishes specific technical development of diagnostic systems and trying to do a review and classification of the various tools and methodologies offered by the field of IT in order to assist the clinical medical diagnosis. Thus, analyzing the various techniques and distinguish the following types of systems based on:

  1. software, which makes analysis of information.
    2. clinical algorithms.
    3. in different mathematical models.
    4. in statistical pattern recognition.
    5. the rule of Vayes.
    6. in theory making.
    7. in symbolic logic approaches.

Recently (2001) Long in the relative study refers to the development of applications of Artificial Intelligence in Medicine looking at various methods of reasoning used by researchers today, registering their organizational structures based on [Long01]. The author argues that the factors which may affect a mechanism of reasoning is the relationship between symptoms and diseases, the chances that have been estimated, the known causes of a disease, the functional (measurement, equations, etc.) and temporary (in relation the time) correlations that may exist, the similarities that make the distinction, the region of the body of the patient and the clinical practice. That is more emphasis in the form of data that support the diagnosis but also the particularities of each disease and not just the mechanical methods that will be used. The Long beyond the dry and unilateral recording some specific methodologies for the representation and use of medical knowledge, giving them a different dimension. Interest now focuses on the benefits and use of support for medical diagnosis systems.

However, it is generally held that the principles of the’90s, researchers had noted that the scope of future applications of Artificial Intelligence in Medicine will depend on the development and operation of integrated systems in the field of Health [Shortliffe92]. These modern facilities will allow the connection of users, the standard registration data, the seamless exchange of digital data, merger or parallel operation and management of knowledge / data, direct access to information and generally are expected to help in proper operation stored information to better inform users of a system of health [Wolfram95, Gardner99, Slack99, Brost99].

 

3.2 Purpose

The diagnosis of epilepsy cases based on the basic characteristics of the type of seizures, which occurs in the patient. Many people may during their lifetime to make a single seizures and in those cases not evaluated the findings. But when there is more of a presence of seizures, it is interesting to diagnose epilepsy. Additionally the doctor will make some tests, which will help the final diagnosis [Ballis98, Cockerell96].
The objective of this diagnostic system is to help the physician to classify an incident seizures in this category of the International Classification [ILAE81, ILAE89] and thereby contribute significantly to the diagnostic procedure that doctors usually follow in cases of epilepsy. Alongside the ability to search similar cases from the database (patient file) will give the opportunity to consider such situations, studying relevant diagnostic procedures and therapeutic methodologies applied. The system will focus on cases of epilepsy that occur during childhood, and where there are more problems of diagnosis and differential diagnosis, as the polymorphism of the disease observed in these ages make the task extremely complicated diagnosis.

 

3.3. Methodology and organization design
It could be described as medical knowledge of the mechanism and implications of physician data is used to reach conclusions. This knowledge, which is required to implement a diagnostic system should be introduced and be represented on the computer in various ways and then utilized by the appropriate software. More generally, for developing systems to support diagnosis, should be taken special care in illustrating the computer system of the thinking of experts, when it will take a decision based on some available data.
The construction of a medical decision support system inevitably follows the classical methodology development projects and concrete should be consistent with the software life cycle, proposed by the Engineering / Software Engineering nformation [Somerville95]. Many researchers, particularly since the’80s, propose methodologies medical diagnostic support systems within the Software Engineering [Breuker87, Szolovits91, Fox93, Healthfield93, Musen97].
In summary, the development of diagnostic support system for child epilepsy, formed in the following 4 key stages of implementation:
1: System Analysis.
2: System Design.
3: Output System.
4: Control System.

 

3.4. Innovation / utility

The growing need for quality health services and the fast renewal of the medical knowledge required by the treating physician to devote much time to examine each case. In practice however, most medical decisions must be taken within a limited time and are usually based on knowledge available at that time in the minds of doctors. Thus the majority of medical decisions are hastily results crisis, as the doctor rarely has the opportunity, mainly due to lack of time to turn to a manual / device to make the literature search or to do extensive research to study a cognitive subject which concerns the case of examining a patient.

The use of computer systems to support medical decision may prove very useful in practice. Systems can provide significant assistance in various phases of the diagnostic process, particularly those where knowledge can be structured and characterized by its objective nature.

The proposed system with the application of Artificial Intelligence technologies and databases to develop the above framework and is expected to be an important aid in the diagnosis of childhood epilepsy especially to young people and their specialized paidonefrologous. It will lay the groundwork for the creation of appropriate infrastructure in TEI Crete, which in future will improve the system under development by use of other technologies of Information and Tele-and probably will develop new systems corresponding to other areas of medicine where there is need for such tools and extensive field research.

 

BIBLIOGRAPHY

[Bossi-Cocco89]A. Bossi, N.Cocco, Verifying Correctness of Logic Programs, Proceedings of International Joint Conference on Theory and Practice of Software Development, Barcelona, Spain, LNCS 352, Vol. 2, pages 96-110, March 1989.
[Brayton94] R. Brayton, HSIS: A BDD-Based Environment for For-mal Verification, in Proc. of the Design Automation Conf., pages 454–459, June 1994.
[Brayton-Hachtel96] R. K. Brayton, G. D. Hachtel, A. L. Sangiovanni-Vincentelli, F. Somenzi, et al., VIS: A System for Verification and Synthesis, Proc. Int. Conf. Computer-Aided Verification, New Brunswick, NJ, July-August 1996.
[Breuker87] Breuker J ed, Model-driven knowledge acquisition interpretation models, ESPRIT Porject 1098, Deliverable Task A1, University of Amsterdam, 1987.
[Brost99] Borst F & others, Happy birthday DIOGENE: a hospital information system born 20 years ago, Medical informatics, 54:157-167, 1999.
[Burstall-Darlington77] R. Burstall and J. Darlington, A Transformation System for Developing Recursive Programs, Journal of ACM, 24(1):44-67, Jan.1977.
[Clark80] K. L. Clark, Predicate Logic as a Computational Formalism, PhD thesis, Queen Mary College, University of London, 1980.
[Clarke-Grumberg94] E. Clarke, O. Grumberg and D. Long, Verification tools for finite-state concurrent systems, in A Decade of Concurrency – Reflections and Perspectives, Lecture Notes in Computer Science, 803, 1994.
[Cockerell96] Cockerell CO, Shorvon Sd, Epilepsy – Current Concepts, Current Medical Literature, 1996.
[Dayantis87] G. Dayantis, Logic Program Derivation for a First Order Logic Relations, Proceedings of the Tenth International Joint Conference on Artificial Intelligence, Vol. 1, Milan, pages 9-14, August, 1987.
[Deville90] Y. Deville, Logic Programming: Systematic Program Development, Addison-Wesley, 1990.
[Flener00] P. Flener, K.-K. Lau, M. Ornaghi and J. Richardson, An Abstract Formalization of Correct Schemas for Program Synthesis, Journal of Symbolic Computation, 20(1):93-127, 2000.
[Fox93] Fox J, Decision Support Systems as Safety-Critical Components: Towards a Safety Culture for Medical Informatics, Meth Inform Med, 32:345-8, 1993.
[Gardner99] Gardner RM et al, The HELP hospital information system: update 1998, Int J of Medical Informatics, 54:169-182, 1999.
[Hansson-Tarnlund79] A. Hansson, S-A. Tarnlund, A Natural Programming Calculus, Proceedings of the Sixth IJCAI, Tokyo, Vol.1, pages 348-355, Aug. 1979.
[Healthfield93] Healthfield HA, Wyatt J, Philosophies for the Design and Development of Clinical Decision-Support Systems, Meth Inform Med, 32:1-8, 1993.
[Hogger81] C. Hogger, Derivation of Logic Programs, Journal of ACM, 28(2):372-392, April 1981.
[ILAE81] Commission on Classification and Terminology of the ILAE, Proposal for revised clinical and electroencephalographic classification of epileptic seizures, Epilepsia, 22:489-501, 1981.
[ILAE89] Commission on Classification and Terminology of the ILAE, Proposal for revised classification of epilepsies and epileptic syndromes, Epilepsia, 30(4):389-399, 1989.
[Jones90] C. Jones, Systematic Software Development Using VDM, Prentice Hall, 1990.
[Krurshan94] Kurshan, R., Computer-Aided Verification of Coordinating Processes – The Automata-Theoretic Approach, Princeton University Press, 1994.
[Long01] Long WJ, Medical Informatics: reasoning methods, Artificial Intelligence in Medicine, 23:71-87, 2001.
[Marakakis97] E. Marakakis, Logic Program Development Based on Typed, Moded Schemata and Data Types, PhD thesis, University of Bristol, February 1997.
[Marakakis-Gallagher94] E. Marakakis, J.P. Gallagher, Schema-Based Top-Down Design of Logic Programs Using Abstract Data Types, LNCS 883, Proceedings of Fourth International Workshops on Logic Program Synthesis and Transformation – Meta-Programming in Logic, edited by L. Fribourg and F. Turini, Pisa, Italy, pages138-153, June 1994.
[Miller94] Miller RA, Medical Diagnostic Decision Support Systems past present and future, J Am Informatics Assoc, 1:8-27, 1994.
[Morgan90] C. Morgan, Programming from Specifications, Prentice Hall, 1990.
[Musen97] Musen MA, Modeling for Decision Support, in Handbook of Medical Informatics, J.H. van Bemmel and M.A. Musen, ed. Springer-Verlag, Heidelberg, 1997.
[Narayan-etal96] Narayan, J. Jain, M. Fujita, and A. L. Sangiovanni-Vincentelli, Partitioned ROBDDs A Compact, Canonical, and Efficiently Manipulatable Representation for Boolean Functions, Proc.IEEE ICCAD, San Jose, CA, November 1996.
[Partsch-Steinbruggen83] H. Partsch and R. Steinbruggen, Program Transformation Systems, Computing Surveys, 15(3):199-236, Sept. 1983.
[Pettorossi-Proietti96] A. Pettorossi, M. Proietti, Rules and Strategies for Transforming Functional and Logic Programs, ACM Computing Surveying, 28(2):360-414, June 1996.
[Pettorossi-Proietti02] A. Pettorossi, M. Proietti, Program Derivation = Rules + Strategies, in A. Kakas and F. Sardi, editors, Computational Logic: Logic Programming and Beyond (Essays in honour of Bob Kowalski, Part I), LNCS 2407, pp. 273-309, Springer, 2002.
[Reisman96] Reisman Y., Computer-based clinical decision aids. A review of methods and assessment of systems, Med. Inform, 21(3):179-197, 1996.
[Shepherdson92] Shepherdson J. C., Unfold/Fold Transformations of Logic Programs, Math. Structure Comput. Sci., 2:143-157, 1992.
[Shortliffe87] Shortliffe EH, Computer Programs to Support Clinical Decision Making, JAMA, 258:61-66, 1987.
[Shortliffe92] Shortliffe EH, The adolescence of AI in Medicine, AIM, 5:93-106, 1992.
[Slack99] Slack WV, Bleich HL, The CCC system in two teaching hospitals: a progress report, Medical Informatics, 54:183-196, 1999.
[Sommerville95] Sommerville I, Software Engineering, Addison-Wesley, 1995
[Spivey92] J.M. Spivey, The Z Notation: A Reference Manual, Prentice-Hall, 1992.
[Szolovits82] Szolovits P, Artificial Intelligence in Medicine, West View Press, Boulder, Colorado, 1982.
[Szolovits91] Szolovits P, Knowledge Based Systems, in Meyer Guttag JV Rivest RL and Slovovits P “Research Directions in Computer Science: An MIT Perspective”, ed. MIT Press, pages 317-370, 1991.
[Tamaki-Sato84] H. Tamaki and T Sato, Unfold/Fold Transformation of Logic Programs, in S.-A Tarnlund (ed), Proceedings of the 2nd International Conference on Logic Programming, Uppsala, Sweden, 1984, pages 127-138.
[Tarnlund79] Sten-Ake Tarnlund, An Axiomatic Data Base Theory, in Logic and Data Bases edited by H. Gallaire and J. Minker, Plenum Press, pages 259-289, 1979.
[Wolfram95] Wolfram DA, An Appraisal of INTERNIST-I, Artificial Intelligence in Medicine, 1995, 7:93-116, 1995.
[www-systemc] www.systemc.org
[Ballis98] J Balis, epilepsy, Chapter 38 of the book “Neuro”, J. Logothetis, University Studio Press, 1998.[:el]Η σκοπιμότητα της πρότασης αφορά τη θεσμοθέτηση εργαστηρίου στο ΤΕΙ Κρήτης που θα προωθεί την επιστημονική έρευνα σε σημαντικά πεδία όπως Τεχνητή Νοημοσύνη και Τεχνολογία Λογισμικού και ειδικότερα σε περιοχές όπως Λογικός Προγραμματισμός, Μεθοδολογία και Σχεδιασμός Συστημάτων και Δικτύων σε Chip, και Ιατρικές Εφαρμογές σε συνεργασία με γνωστά διεθνώς Πανεπιστήμια, Ερευνητικά Κέντρα και Εταιρείες. Οι δραστηριότητες αυτού του υποέργου αντιστοιχούν στις προαναφερθείσες περιοχές. Ελπίζουμε ότι αυτό το υποέργο θα βοηθήσει στην ανάπτυξη της έρευνας, και ιδιαίτερα στην καλύτερη ερευνητική παρουσία, την θεσμοθέτηση και στη βελτίωση της υποδομής του υπάρχοντος εργαστηρίου ¨”Τεχνητής Νοημοσύνης και Τεχνολογίας Λογισμικού” του ΤΕΙ Κρήτης. Επίσης η συνεργασία με κορυφαία Πανεπιστήμια και ιδιαίτερα με Εταιρείες, νομίζουμε ότι θα αναδείξει σημαντικά την Εφαρμοσμένη Τεχνολογική Έρευνα στο ΤΕΙ Κρήτης.

 

Δραστηριότητα 1 : Εργαλεία Μετασχηματισμού και Επαλήθευσης Προγραμμάτων

Η ανάπτυξη λογισμικού είναι μια δραστηριότητα η οποία συχνά αρχίζει από μια άτυπη και ασαφή απαίτηση του τι χρειάζεται να γίνει και καταλήγει σ’ ένα πολύ λεπτομερές τυπικό αντικείμενο το σύστημα λογισμικού. Η διαδικασία ανάπτυξης λογισμικού απαιτεί πολύ εργασία, παράλληλα είναι επιρρεπής σε λάθη. Επιπλέον, το τελικό αποτέλεσμα δεν περιέχει την σχεδιαστική γνώση η οποία οδήγησε στην κατασκευή του λογισμικού συστήματος. Αυτή η σχεδιαστική γνώση χρειάζεται να συντηρείται και να ενημερώνεται ώστε να επαναχρησιμοποιείται για την ανάπτυξη νέων συστημάτων λογισμικού.

Υπάρχουν μεθοδολογίες ανάπτυξης λογισμικού οι οποίες κατασκευάζουν πολύ δομημένα προγράμματα [Μarakakis94, Marakakis97]. Τα κατασκευαζόμενα προγράμματα απεικονίζουν τις σχεδιαστικές αποφάσεις οι οποίες έχουν ακολουθηθεί κατά την κατασκευή του. Αυτές οι μεθοδολογίες κατασκευάζουν ένα εκτελέσιμο σχέδιο προγράμματος παρά ένα αποτελεσματικό πρόγραμμα. Α αποτελεσματικότητα δεν είναι ένα θέμα το οποίο πρέπει να λαμβάνεται υπόψη κατά την φάση κατασκευή του προγράμματος. Τα πλεονεκτήματα τέτοιων μεθοδολογιών είναι τα εξής: 1) Το κατασκευαζόμενο πρόγραμμα λόγω της πολύ δομημένης του μορφής μπορεί να χρησιμοποιείται για συντήρηση του προγράμματος και για απόδειξη ιδιοτήτων του προγράμματος. Αλλαγές στο πρόγραμμα μπορούν να γίνονται στο επίπεδο των αποφάσεων σχεδίασης. Δηλαδή, αλλαγή στο πρόγραμμα σημαίνει αλλαγή σ’ ένα σύνολο αποφάσεων σχεδίασης. 2) Η απόδειξη της ορθότητας των κατασκευαζόμενων προγραμμάτων διευκολύνεται από την πολύ δομημένη μορφή τους. 3) Ένα εργαλείο μπορεί να κατασκευαστεί το οποίο αυτόματα θα μετασχηματίζει τα δομημένα προγράμματα σε αντίστοιχα πιο αποτελεσματικά και μικρότερου μεγέθους τα οποία θα χρησιμοποιούνται για τρέξιμο.

Αυτό το υποέργο σκοπεύει στην ανάπτυξη εργαλείων χρησιμοποιώντας τεχνικές Τεχνητής Νοημοσύνης τα οποία θα αυξήσουν και θα δείξουν την ισχύ τέτοιων κατασκευαστικών μεθόδων λογισμικού [Marakakis94, Marakakis97]. Επιπλέον, θα μελετηθούν οι τομείς του μετασχηματισμού προγραμμάτων καθώς και της επαλήθευσης προγραμμάτων. Στοχεύουμε στην ανάπτυξη των εξής εργαλείων: 1) Κατασκευή ενός αυτόματου ή ημιαυτόματου εργαλείου το οποίο θα μετασχηματίζει τα πολύ δομημένα προγράμματα σε αντίστοιχα πιο συμπαγή (μικρότερος κώδικας) και πιο αποτελεσματικά προγράμματα. 2) Ανάπτυξη ενός διαλογικού επαληθευτή (verifier) o οποίος θα αποδεικνύει την ορθότητα των κατασκευαζόμενων προγραμμάτων. Επιπλέον, θα μελετηθεί η σχέση η οποία μπορεί να υπάρχει στην δομή των κατασκευαζόμενων προγραμμάτων και στην δομή της απόδειξης της ορθότητας τους.

Το λογισμικό που θα κατασκευαστεί καθώς και η μέθοδος κατασκευής λογικών προγραμμάτων [Marakakis94, Marakakis97] θα χρησιμοποιηθούν σε μαθήματα σχετικά με την ανάπτυξη λογισμικού (Προγρ/σμός ΙΙ, Τεχνολογία Λογισμικού). Επιπλέον, θα υλοποιηθούν προχωρημένες τεχνικές Τεχνητής Νοημοσύνης. Αυτές θα αξιοποιηθούν εκπαιδευτικά στο μάθημα Τεχνητή Νοημοσύνη. Στοχεύουμε να έλθουμε σε επαφή με εταιρίες ανάπτυξης λογισμικού οι οποίες θα αξιοποιήσουν περισσότερο τ’ αποτελέσματα αυτής της δραστηριότητας.

 

1.1. Μετασχηματισμός λογικών προγραμμάτων σε αντίστοιχα πιο αποτελεσματικά και μικρότερου μεγέθους.

Η πρώτη εργασία για μετασχηματισμό προγραμμάτων κατά την ανάπτυξη λογισμικού αναφέρεραι στο άρθρο των Burstall και Darlington [Burstall-Darlington77]. Στην πιο γενική του μορφή ένα μετασχηματισμός είναι μια σχέση μεταξύ δύο σχημάτων προγραμμάτων Σ και Σ’. Ο μετασχηματισμός θεωρείται σωστός εάν κάποια σημασιολογική σχέση ισχύει μεταξύ του Σ και Σ’ [Partsch-Steinbruggen83]. Η πιο σημαντική σημασιολογική σχέση είναι της ισοδυναμίας.

Το πρώτο σύστημα μετασχηματισμού για λογικά προγράμματα χωρίς άρνηση βασισμένο στους μετασχηματισμούς πτύξη (fold) – ανάπτυξη (unfold) αναπτύχθηκε από τον Tamaki και Sato [Tamaki-Sato84]. Στο άρθρο [Shepherdson92] γίνεται επέκταση των αποτελεσμάτων του Tamaki και Sato σε κανονικά λογικά προγράμματα όπου αρνητικοί στοιχειώδεις τύποι (literals) επιτρέπονται στο σώμα των προτάσεων. Βελτίωση στην αποτελεσματικότητα δεν εξασφαλίζεται όταν οι κανόνες μετασχηματισμού εφαρμόζονται απειθάρχητα χωρίς κάποια ιδιαίτερη σειρά. Γι’ αυτό το λόγο εισήχθησαν οι στρατηγικές μετασχηματισμών από τους Pettorossi και Proietti [Pettorossi-Proietti96], [Pettorossi-Proietti02]. Οι στρατηγικές μετασχηματισμών είναι μετα-κανόνες οι οποίοι κατευθύνουν την εφαρμογή των κανόνων μετασχηματισμού επιβάλοντας την εφαρμογή κατάληλων ακολουθιών κανόνων μετασχηματισμού έτσι ώστε να βελτιώνεται η αποτελεσματικότητα των παραγόμενων προγραμμάτων.

Ο στόχος του μετασχηματισμού προγραμμάτων είναι η βελτίωση της αποτελεσματικότητας ενώ ταυτόχρονα να διατηρείται η σημασιολογία του προγράμματος. Ο μετασχηματισμός αρχίζει από ένα αρχικό πρόγραμμα, Π0, και μετά ένας ή περισσότεροι στοιχειώδεις κανόνες μετασχηματισμών εφαρμόζονται. Έτσι, παίρνουμε μια ακολουθία Π0,..,Πν από προγράμματα. Εμείς θέλουμε το τελικό πρόγραμμα Πν να έχει την ίδια σημασιολογία με το αντίστοιχο αρχικό Π0. Αυτό επιτυγχάνεται εάν εφαρμόσομε κανόνες μετασχηματισμών οι οποίοι διατηρούν την σημασιολογία. Δηλαδή, για δύο προγράμματα Π και Ρ, σημασιολογία(Π) = σημασιολογία(Ρ) ισχύει εάν το Ρ μπορεί να παραχθεί από το Π με μια εφαρμογή ενός μόνο κανόνα μετασχηματισμών [Pettorossi-Proietti96], [Pettorossi-Proietti02]. Εμείς συνήθως θέλουμε το Πν να είναι περισσότερο αποτελεσματικό από το Π0. Θα μελετήσουμε μεταξύ άλλων και τους εξής κανόνες μετασχηματισμού λογικών προγραμμάτων. 1) Κανόνας νέου ορισμού. 2) Κανόνας ανάπτυξης (unfold). 3) Κανόνας πτύξης (fold). 4) Κανόνας αντικατάστασης στόχου. 5) Κανόνας διαγραφής πρότασης.

Η μη αποτελεσματικότητα των προγραμμάτων που κατασκευάζονται με την μέθοδο [Marakakis94, Marakakis97] μπορεί να οφείλεται στην πολύ δομημένη μορφή τους. Η αναποτελεσματικότητα αυτών των προγραμμάτων μπορεί να διορθωθεί εφαρμόζοντας κανόνες μετασχηματισμού λογικών προγραμμάτων όπως οι προαναφερθέντες. Ο στόχος αυτών των μετασχηματισμών είναι να αφαιρέσουν από τα προγράμματα το σχεδιαστικό επίπεδο με αποτέλεσμα το μέγεθος τους να ελαττωθεί αλλά και να τα κάνει περισσότερο αποτελεσματικά.

 

1.2. Επαληθευτής Λογικών Προγραμμάτων

Υπάρχουν δύο προσεγγίσεις στο πρόβλημα της ορθότητας ενός προγράμματος. Η μια προσέγγιση περιλαμβάνει εξέταση του προγράμματος μ’ ένα πεπερασμένο σύνολο ελέγχων. Οι έλεγχοι μπορούν να δείξουν ότι ένα πρόγραμμα δεν έχει λάθη για ένα δοσμένο πεπερασμένο σύνολο ελέγχων. Για προγράμματα με πολύπλοκη είσοδο/έξοδο είναι δύσκολο να δείξεις την ορθότητα του ή όχι. Εξέταση ενός προγράμματος δεν μπορεί να δείξει πλήρη απουσία λαθών. Η άλλη προσέγγιση είναι ν’ αποδείξεις ότι ένα πρόγραμμα είναι ορθό σε σχέση με τις προδιαγραφές του με τυπικούς συλλογισμούς.

Θεωρώντας ότι η προδιαγραφή ενός προγράμματος είναι δεδομένη υπάρχουν δύο κύριες προσεγγίσεις για απόδειξη της ορθότητας του. Στην πρώτη προσέγγιση, η ορθότητα εξασφαλίζεται κατά την κατασκευή του προγράμματος [Deville90, Flener00, Hogger81, Morgan90]. Σ’ αυτή την περίπτωση μια προδιαγραφή βελτιώνεται διαδοχικά σ’ ένα πρόγραμμα. Η διαδικασία κατασκευής συνίσταται είτε από μικρότερα προκαθορισμένα βήματα ανάπτυξης των οποίων η ορθότητα έχει αποδειχθεί ή από μετασχηματισμούς οι οποίοι διατηρούν την ισοδυναμία, δηλαδή μετασχηματίζουν μια προδιαγραφή ή πρόγραμμα σε άλλη ισοδύναμη μορφή. Στην δεύτερη προσέγγιση, ένα πρόγραμμα πρώτα κατασκευάζεται με κάποια μεθοδολογία και μετά αποδεικνύεται η ορθότητα του σε σχέση με την προδιαγραφή του [Bossi-Cocco89, Clark80].

Η λογική πρώτης τάξεως (ΛΠΤ) είναι ένας συνηθισμένος φορμαλισμός για προδιαγραφή προγραμμάτων στον διαδικαστικό, λογικό και συναρτησιακό προγραμματισμό. Τα όρια μεταξύ προδιαγραφών και προγραμμάτων δεν είναι αυστηρά στις γλώσσες του λογικού προγραμματισμού. Το πλεονέκτημα τους σε σύγκριση με τις διαδικαστικές γλώσσες προγραμματισμού είναι η εγγύτητα τους στην λογική πρώτης τάξης. Η χρήση του ίδιου φορμαλισμού για προδιαγραφές και για προγράμματα διευκολύνει την επαλήθευση των προγραμμάτων καθώς και την παραγωγή προγραμμάτων από προδιαγραφές.

Στην βιβλιογραφία υπάρχουν αρκετές προσεγγίσεις επαλήθευσης προγραμμάτων οι οποίες χρησιμοποιούν την ΛΠΤ σαν την γλώσσα προδιαγραφών [Clark80, Dayantis87, Deville90, Hansson-Tarnlund79, Tarnlund79]. Σ’ αυτές τις προσεγγίσεις μια προδιαγραφή αποτελείται από ένα σύνολο τύπων της ΛΠΤ. Κάθε τύπος εκφράζει την προδιαγραφή μιας σχέσης η οποία μπορεί να εκφράζεται συναρτήσει άλλων σχέσεων μέχρι του επιπέδου βασικών τμημάτων. Μια τυπική προδιαγραφή στην ΛΠΤ ονομάζεται λογική προδιαγραφή.

Οι τύποι (types) είναι ένα σημαντικό τμήμα των προδιαγραφών. Η φύση της γνώσης που εμπλέκεται στις προδιαγραφές περιέχει τύπους. Προδιαγραφές οι οποίες στηρίζονται στην λογική και δεν περιέχουν τύπους δεν είναι αρκετά εκφραστικές για προδιαγραφή μεγάλων συστημάτων λογισμικού. Δημοφιλείς γλώσσες προδιαγραφών οι οποίες στοχεύουν για προδιαγραφή σύνθετων συστημάτων λογισμικού χρησιμοποιούν λογική με τύπους [Jones90, Spivey92].

Μια λογική προδιαγραφή στη δική μας προσέγγιση ουσιαστικά ακολουθεί τις προσεγγίσεις οι οποίες βασίζονται στην ΛΠΤ αλλά επιπλέον χρησιμοποιεί ΛΠΤ με τύπους και ισότητα. Στοχεύουμε στην ανάπτυξη ενός ημιαυτόματου επαληθευτή για απόδειξη της ορθότητας λογικών προγραμμάτων τα οποία κατασκευάζονται από τη μεθοδολογία [Marakakis94, Marakakis97] σε σχέση με την προδιαγραφή τους η οποία εκφράζεται σε ΛΠΤ με τύπους. Ο επαληθευτής θα κατευθύνεται από τον προγραμματιστή. Δηλαδή, ο προγραμματιστής θα επιλέγει εξαγωγές συμπερασμάτων (inferences) και ο επαληθευτής θα τις εκτελεί. Βλέπουμε ένα τέτοιο επαληθευτή να γίνεται περισσότερο αυτόματος σταδιακά μετακινώντας αποφάσεις απόδειξης από τον προγραμματιστή στο σύστημα. Ο επαληθευτής θα μπορεί να αποδεικνύει λήμματα τα οποία στη συνέχεια θα μπορούν να χρησιμοποιούνται σε επόμενες αποδείξεις. Ο επαληθευτής εκτός από εξαγωγές συμπερασμάτων πρώτης τάξεως θα μπορεί να εκτελεί και επαγωγικές αποδείξεις.

 

Δραστηριότητα2: Πιστοποίηση συστημάτων και δικτύων επικοινωνίας σε chip

Γιά την ανεύρεση λαθών, σύνθετα συστήματα, όπως το σύστημα σε chip ή δίκτυο επικοινωνίας σε chip (system-on-chip, network on-chip), συνήθως διεξάγονται δυο τρόποι ελέγχου:

– Επαλήθευση (verification). Κατά την επαλήθευση το σύστημα ελέγχεται κατά πόσον αναπτύσσεται σωστά, σύμφωνα με τις προδιαγραφές. Η επαλήθευση γίνεται όταν υπάρχει ένα τμήμα τελειωμένο που εργάζεται κανονικά και συνήθως ο έλεγχος ακολουθεί το μοντέλο κύκλου λογισμικού (software cycle model).

– Πιστοποίηση (validation): Η διαδικασία της πιστοποίησης διαπιστώνει ότι το σύστημα που αναπτύσσεται είναι αυτό που ο πελάτης και ο τελικός χρήστης επιθυμούν. Η πιστοποίηση που γίνεται για κάθε περίπτωση χρήσης, συνήθως χρησιμοποιεί προσομοίωση (simulation) για να εξετάσει τις αλληλεπιδράσεις με το σύστημα. Έτσι αποστέλλει η λαμβάνει μηνύματα προς/από το σύστημα ή εναλλάσσει πληροφορίες με το σύστημα, με σκοπό να ελέγξει την αρχικοποίηση κάθε υποσυστήματος, να εξετάσει τη χρονική ροή των μηνυμάτων (events, messages) όπως και εναλλακτικές ροές γεγονότων, και να τσεκάρει την ισοδυναμία των αποτελεσμάτων κάθε προβλεπόμενης χρήσης

Υπάρχουν πολλά ανοικτά προβλήματα που σχετίζονται με τις δραστηριότητες επαλήθευσης υποσυστημάτων και πιστοποίησης συστημάτων σε chip ή δικτύων επικοινωνίας σε chip

• Τα υπάρχοντα μοντέλλα υποσυστημάτων (λογισμικό) συχνά αναπτύσσονται και ελέγχονται με διαφορετικά εργαλεία, που οδηγεί σε ένα ετερογενές περιβάλλον. Έτσι μόνο η συμβατότητα (interoperability) εργαλείων πολύπλοκων και διαφορετικών καθώς και γλωσσών μπορεί να δώσει δυνατότητες επαναχρησιμοποίησης (software reuse).

• Τα μοντέλα του συστήματος που μπορεί να συνυπάρχουν σε διαφορετικά επίπεδα αφαίρεσης (abstraction levels) απαιτούν ξεχωριστή επαλήθευση και πιστοποίηση.

• Η αποδοτική μοντελοποίηση συστήματος απαιτεί παράλληλη ή κατανεμημένη προσομοίωση.

• Τα υπάρχοντα εργαλεία επαλήθευσης (στο επίπεδο συστήματος ή μπλόκ) είναι εξαρτημένα από την υλοποίηση, και δεν είναι εύκολο να αλλαχθούν παράμετροι αρχιτεκτονικής χωρίς να ξανασχεδιαστεί εξαρχής το περιβάλλον επαλήθευσης.

Η πρώτη γενιά εργαλείων για αυτόματη επαλήθευση βασίστηκε σε μεθόδους μοντελοποίησης χρονικής λογικής (temporal logic). Το σύστημα (κύκλωμα ή διαδικασία) περιγράφεται ως μια μηχανή πεπερασμένων καταστάσεων (finite state machine), ενώ οι ιδιότητες του εκφράζονται σαν τύποι χρονικής λογικής με δυνατότητες έκφρασης αλληλοσυσχέτισης (mutual exclusion), ταυτόχρονης προσπέλασης, και δικαιοσύνης (fairness). Ένα παράδειγμα αποτελεί το σύστημα SMV που αναπτύχθηκε στο Carnegie Mellon University και χρησιμοποιεί λογική υπολογιστικού δένδρου (Computational Tree Logic, ή CTL) [Clarke-Grumberg94]. Η τεχνική αυτή έχει χρησιμοποιηθεί επιτυχώς, π.χ. για την επαλήθευση συστημάτων λεωφορείων όπως Futurebus και PCI local bus.

Μερικές ιδιότητες δεν εκφράζονται σε CTL, αλλά μπορούν να εκφραστούν σαν πεπερασμένα αυτόματα (και αντίστροφα) . Έτσι μια δεύτερη θεώρηση χρησιμοποιεί την μέθοδο υποσυνόλου γλωσσών (language containment) για να ελέγξει ότι οι ιδιότητες του συστήματος που εκφράζονται σαν πεπερασμένα αυτόματα περιέχουν τις απαραίτητες σχέσεις. Το σύστημα COSPAN, αναπτύχθηκε πειραματικά από τα Bell Labs, και χρησιμοποιείται τώρα από εργαλεία της Cadence [Krurshan94]. Πρέπει επίσης να τονίσουμε ότι το σύστημα HSIS που αναπτύχθηκε στο Παν. Berkeley χρησιμοποιεί ένα συνδυασμό των δύο τεχνικών [Brayton94, Brayton-Hachtel96].

Τα περισσότερα λάθη που ανακαλύπτονται κατά τη διάρκεια της προσομοίωσης θα μπορούσαν να είχαν ανακαλυφθεί πιό νωρίς, με μικρότερο κόστος με τεχνικές ανάλυσης και προσομοίωσης υψηλού επιπέδου. Εμείς θα μελετήσουμε ένα φιλικό προς το χρήστη, περιβάλλον πιστοποίησης, σχεδιάζοντας και υλοποιώντας ένα παράλληλο ή κατανεμημένο εργαλείο στατικής και δυναμικής ανάλυσης που δίνει δυνατότητες επαλήθευσης ιδιοτήτων συστήματος με βάσεις τις απαιτήσεις χρηστών. Το εργαλείο αυτό, βασισμένο σε θεωρία γράφων και συνδυαστικές μεθόδους (combinatorics), θα μπορεί επίσης να επιβεβαιώνει συνθήκες πραγματικού χρόνου σε σύνθετα, πιθανώς ασύγχρονα μοντέλα συστημάτων με τη χρήση εφικτών πινάκων (reachability matrices), ή με υπολογισμούς αξιοπιστίας (reliability).

Πιο συγκεκριμένα, τα τεχνικά θέματα που θα μελετηθούν περιλαμβάνουν τεχνικές ταυτόχρονης προσπέλασης (concurrency) και ανάκαμψης (recovery) για το σχεδιασμό προηγμένων παράλληλων και κατανεμημένων δομών δεδομένων και αλγορίθμων [Narayan-etal96]. Θα βασιστούμε στη θεωρία γράφων (graph theory), τη συνδυαστική (combinatorics), τις πιθανότητες (probabilistic algorithms), και τεχνικές τεχνητής νοημοσύνης, που να μπορούν να χρησιμοποιηθούν για την αναπαράσταση περιορισμών και την πιστοποίηση συστημάτων ή δικτύων επικοινωνίας σε chip. Ειδικότερα, θα χρησιμοποιήσουμε σαν βάση την αντικειμενοστραφή μοντελοποίηση συστημάτων με το νέο βιομηχανικό στάνταρντ SystemC2.0 [www-systemc]. Το κυρίως ανοικτού κώδικα λογισμικό που θα χρησιμοποιηθεί αρχικά αποτελείται από νέα εργαλεία επαλήθευσης και προσομοίωσης συστημάτων σε chip, π.χ. o Τestbuilder της Cadence, το στάνταρντ SCV (SystemC Verification Library) [www-systemc], καθώς και πρόσφατα άρθρα που αναφέρονται σε συγκεκριμένες η γενικότερες τεχνικές πιστοποίησης συστημάτων, όπως αναφέρουμε παρακάτω

. Το προγραμματιστικό περιβάλλον που θα υλοποιηθεί θα χρησιμοποιηθεί και σε αντίστοιχα μαθήματα επιλογής του TEI ώστε να γίνει αποτίμηση των συνδυαστικών/ ευρηματικών τεχνικών (combinatorics, heuristics) και να βελτιωθεί η αποδοτικότητα του συστήματος με νέους αποδοτικότερους αλγορίθμους. Επίσης ελπίζουμε σε συνεργασία με την βιομηχανία για την κατάλληλη αξιοποίηση του.

 

Δραστηριότητα 3: Πληροφοριακό Σύστημα Υποστήριξης για την Διάγνωση Παιδικής Επιληψίας

 

3.1 Επισκόπιση ερευνητικού αντικειμένου

Κατά την διάρκεια των τριάντα τελευταίων χρόνων έχουν πραγματοποιηθεί αξιόλογες ερευνητικές προσπάθειες για την ανάπτυξη μεθόδων ικανών να αντιμετωπίσουν πολύπλοκα προβλήματα, όπως αυτά που σχετίζονται με την ιατρική διάγνωση.

Το πρώτο εμπεριστατωμένο βιβλίο το οποίο αναφερόταν στις τεχνικές ανάπτυξης συστημάτων που υποστηρίζουν την ιατρική διάγνωση, γράφτηκε από το Szolovits και εκδόθηκε το 1982 με τον τίτλο «Τεχνητή Νοημοσύνη στην Ιατρική» [Szolovits82]. Αυτή η έκδοση, έκανε μία εκτενή αναφορά στα πρώτα συστήματα υποστήριξης διάγνωσης, παρουσιάζοντας τις μεθοδολογίες που είχαν αναπτυχθεί μέχρι τότε και απετέλεσε την αφετηρία για την έρευνα στον συγκεκριμένο τομέα την δεκαετία που ακολούθησε.

Βέβαια κατά κάποιο τρόπο κάθε σύστημα πληροφορικής το οποίο έχει να κάνει με διαχείριση κάποιων ιατρικών δεδομένών ή με την αναπαραγωγή της ιατρικής γνώσης, μπορεί να θεωρηθεί ότι συμβάλει στην κλινική διάγνωση. Έτσι ο Shortliffe [Shortliffe87] αναφέρει ότι υπάρχουν τρεις βασικές μορφές συστημάτων πληροφορικής, τα οποία μπορούν να προσφέρουν βοήθεια στην διαδικασία της διάγνωσης:

1. Συστήματα πληροφορικής που κάνουν απλή διαχείριση δεδομένων.

2. Συστήματα που έχουν σαν στόχο να προσελκύσουν την προσοχή του χρήστη σε ορισμένα σημεία κατά την διάρκεια της διάγνωσης.

3. Συμβουλευτικά συστήματα πληροφορικής τα οποία στηρίζονται σε πληροφορίες που αφορούν συγκεκριμένες περιπτώσεις ασθενών (patient-specific).

Το 1994 ο Miller [Miller94] παρουσιάζει μία εκτενή μελέτη για την πορεία των συστημάτων που υποστηρίζουν την ιατρική διάγνωση. Σε αυτή την έρευνα αναφέρονται όλες σχεδόν οι προσπάθειες των ερευνητών μέχρι τότε, καταδεικνύοντας το ενδιαφέρον που παρουσιάζει ο συγκεκριμένος τομέας. Στο τέλος του εν λόγω άρθρου ο συγγραφέας καταλήγει με την πρόβλεψη ότι το μέλλον των συστημάτων υποστήριξης ιατρικών αποφάσεων (MDDS) διαγράφεται μακρινό και ότι ο αριθμός των ερευνητών στο συγκεκριμένο πεδίο θα αυξάνεται συνεχώς. Διαβλέπει δε σημαντικό εμπορικό ενδιαφέρον από εταιρείες του χώρου για αυτού του είδους τα συστήματα και ότι καθώς θα προχωρά η τεχνολογία της Πληροφορικής θα γίνεται ολοένα πιο συμφέρουσα διαχείριση των κλινικών δεδομένων για μία αποτελεσματικότερη περίθαλψη υγείας.

Λίγο αργότερα, ο Υ Reedman σε σχετικό του άρθρο [Reisman96] διακρίνει συγκεκριμένες τεχνικές ανάπτυξης διαγνωστικών συστημάτων πληροφορικής και προσπαθεί να κάνει μία επισκόπηση και ταξινόμηση των διάφορων εργαλείων και μεθοδολογιών, που προσφέρονται από τον τομέα της Πληροφορικής με στόχο να βοηθήσουν την κλινική ιατρική διάγνωση. Έτσι αναλύει τις διάφορες τεχνικές και διακρίνει τις ακόλουθες κατηγορίες συστημάτων που στηρίζονται σε :

1. σε λογισμικό το οποίο κάνει ανάλυση βάσεων πληροφοριών.
2. σε κλινικούς αλγορίθμους.
3. σε διάφορα μαθηματικά μοντέλα.
4. στην στατιστική αναγνώριση προτύπων.
5. στον κανόνα του Βayes.
6. στην θεωρία λήψης αποφάσεων.
7. σε συμβολικές λογικές προσεγγίσεις.

Πρόσφατα (2001) ο Long σε σχετική του μελέτη αναφέρεται στην εξέλιξη των εφαρμογών της Τεχνητής Νοημοσύνης στην Ιατρική εξετάζοντας διάφορες μεθοδολογίες συλλογισμού που χρησιμοποιούνται από τους ερευνητές σήμερα, καταγράφοντας τις οργανωτικές δομές στις οποίες στηρίζονται [Long01]. Ο συγγραφέας υποστηρίζει ότι τα στοιχεία τα οποία μπορούν να επηρεάσουν έναν μηχανισμό συλλογισμού είναι οι σχέσεις μεταξύ συμπτωμάτων και ασθενειών, οι πιθανότητες που έχουν εκτιμηθεί, οι γνωστές αιτίες που προκαλούν μια ασθένεια, οι λειτουργικές (μετρήσεις, εξισώσεις κλπ) και προσωρινές (που έχουν σχέση με την χρόνο) συσχετίσεις που μπορούν να υπάρχουν, οι ομοιότητες που δυσκολεύουν την διάκριση, η περιοχή του σώματος του ασθενούς και η κλινική πρακτική. Δηλαδή δίνεται μεγαλύτερη έμφαση στην μορφή των δεδομένων που θα στηριχθεί η διάγνωση αλλά και στις ιδιαιτερότητες κάθε ασθένειας και όχι απαραίτητα μόνο στην μηχανιστική μεθοδολογία της πληροφορικής που θα χρησιμοποιηθεί. Ο Long ξεφεύγει από την «άχαρη» και μονομερή καταγραφή κάποιων συγκεκριμένων μεθοδολογιών για την αναπαράσταση και την εκμετάλλευση της ιατρικής γνώσης, δίνοντας τους μία διαφορετική διάσταση. Το ενδιαφέρον πλέον εστιάζεται στην ωφελιμότητα και στην χρήση αυτών των υποστηρικτικών για την ιατρική διάγνωση συστημάτων.

Πάντως, είναι γενική διαπίστωση ότι από τις αρχές τις δεκαετίας του 90, ερευνητές είχαν επισημάνει ότι το μέλλον του πεδίου των εφαρμογών της Τεχνητής Νοημοσύνης στην Ιατρική θα εξαρτηθεί από την ανάπτυξη και λειτουργία ολοκληρωμένων συστημάτων πληροφορικής στον τομέα της Υγείας [Shortliffe92]. Αυτές οι σύγχρονες υποδομές, θα επιτρέψουν την σύνδεση των χρηστών, την τυποποιημένη καταχώρηση στοιχείων, την απρόσκοπτη ανταλλαγή ψηφιακών δεδομένων, την συγχώνευση ή την παράλληλη λειτουργία και διαχείριση βάσεων γνώσεων / δεδομένων, την άμεση πρόσβαση σε πληροφόρηση και γενικότερα αναμένεται να βοηθήσουν σημαντικά στην κατάλληλη εκμετάλλευση των αποθηκευμένων πληροφοριών για την πληρέστερη ενημέρωση των χρηστών ενός συστήματος υγείας [Wolfram95, Gardner99, Slack99, Brost99].

 

3.2 Σκοπός

Η διάγνωση περιπτώσεων επιληψίας βασικά στηρίζεται στα χαρακτηριστικά του τύπου της επιληπτικής κρίσης, η οποία παρατηρείται στον ασθενή. Πολλοί άνθρωποι είναι δυνατόν κατά την διάρκεια της ζωής τους να παρουσιάσουν κάποια μεμονωμένη επιληπτική κρίση και σε αυτές τις περιπτώσεις δεν αξιολογείται το εύρημα. Όταν όμως παρατηρείται παρουσία περισσότερων της μίας επιληπτικών κρίσεων, τότε παρουσιάζει ενδιαφέρον η διάγνωση της επιληψίας. Επιπλέον ο ιατρός θα προβεί σε ορισμένες εξετάσεις, οι οποίες θα τον βοηθήσουν στην τελική του διάγνωση [Μπαλλής98, Cockerell96].
Στόχος του συγκεκριμένου διαγνωστικού συστήματος, είναι να βοηθήσει τον γιατρό να κατατάξει ένα περιστατικό επιληπτικής κρίσης σε συγκεκριμένη κατηγορία της διεθνούς ταξινόμησης [ILAE81,ILAE89] και κατά συνέπεια να συμβάλει σημαντικά στην διαγνωστική διαδικασία που συνήθως ακολουθούν οι ιατροί σε περιπτώσεις επιληψίας. Παράλληλα η δυνατότητα αναζήτησης παρόμοιων περιστατικών από την βάση δεδομένων (φάκελος ασθενούς) θα του δίνει την ευκαιρία να εξετάζει ανάλογες καταστάσεις, μελετώντας αντίστοιχες διαγνωστικές διαδικασίες, και θεραπευτικές μεθοδολογίες που εφαρμόστηκαν. Το σύστημα θα εστιάσει σε περιπτώσεις επιληψιών που παρουσιάζονται κατά την διάρκεια της παιδικής ηλικίας, όπου και υπάρχουν τα περισσότερα προβλήματα διάγνωσης και διαφορικής διάγνωσης, καθώς ο πολυμορφισμός της ασθένειας που παρατηρείται σε αυτές τις ηλικίες καθιστούν το έργο της διάγνωσης εξαιρετικά πολύπλοκο.

 

3.3. Μεθοδολογία οργάνωσης & σχεδιασμού
Θα μπορούσαμε να χαρακτηρίσουμε σαν ιατρική γνώση τον μηχανισμό της συνεπαγωγής του ιατρού και τα δεδομένα που χρησιμοποιεί αυτός για να φτάσει σε συμπεράσματα. Αυτή η γνώση, η οποία απαιτείται για την υλοποίηση ενός διαγνωστικού συστήματος, πρέπει να εισαχθεί και να αναπαρασταθεί στον υπολογιστή με διάφορους τρόπους και στην συνέχεια να αξιοποιηθεί κατάλληλα από το λογισμικό. Γενικότερα, για την ανάπτυξη συστημάτων υποστήριξης διάγνωσης, θα πρέπει να ληφθεί ιδιαίτερη μέριμνα για την αποτύπωση στο υπολογιστικό σύστημα του τρόπου σκέψης του ειδήμονα, όταν αυτός πρόκειται να λάβει κάποια απόφαση στηριζόμενος σε ορισμένα διαθέσιμα δεδομένα.
Η κατασκευή ενός συστήματος υποστήριξης αποφάσεων ιατρικής, μοιραία ακολουθεί την κλασική μεθοδολογία ανάπτυξης έργων Πληροφορικής και συγκεκριμένα θα πρέπει να εναρμονίζεται με τον κύκλο ζωής λογισμικού, που προτείνεται από τον τομέα της «Μηχανικής/Τεχνολογίας Λογισμικού» της Πληροφορικής [Somerville95]. Πολλοί ερευνητές, ιδιαίτερα μετά την δεκαετία του 80, προτείνουν μεθοδολογίες ανάπτυξης συστημάτων στήριξης ιατρικής διάγνωσης στα πλαίσια της Μηχανικής Λογισμικού [Breuker87, Szolovits91, Fox93, Healthfield93, Musen97].
Συνοπτικά, η ανάπτυξη του συστήματος υποστήριξης διάγνωσης για την παιδική επιληψία, διαμορφώνεται στα εξής 4 βασικά στάδια υλοποίησης:
1: Ανάλυση Συστήματος.
.2: Σχεδιασμός Συστήματος.
3: Υλοποίηση Συστήματος.
4: Ελεγχος Συστήματος.

 

3.4. Καινοτομία / χρησιμότητα

Οι αυξανόμενες ανάγκες για παροχή ποιοτικών υπηρεσιών υγείας αλλά και η με ταχείς ρυθμούς ανανέωση της ιατρικής γνώσης, απαιτούν από τον θεράποντα ιατρό να αφιερώνει μεγάλο χρόνο σε κάθε περίπτωση που εξετάζει. Στην πράξη όμως οι περισσότερες ιατρικές αποφάσεις πρέπει να ληφθούν μέσα σε περιορισμένο χρονικό διάστημα και συνήθως είναι βασισμένες σε γνώση που υπάρχει εκείνη την στιγμή στο μυαλό του ιατρού. Έτσι στην πλειοψηφία τους οι ιατρικές αποφάσεις είναι αποτελέσματα βιαστικών κρίσεων, καθώς ο ιατρός σπάνια έχει την ευκαιρία, λόγω έλλειψης χρόνου κυρίως, να απευθυνθεί σε κάποιο εγχειρίδιο / βοήθημα, να προβεί σε αναζήτηση σχετικής βιβλιογραφίας ή να κάνει εκτεταμένες έρευνες για να μελετήσει διεξοδικά κάποιο γνωστικό αντικείμενο το οποίο αφορά την περίπτωση του ασθενούς που εξετάζει.

Η χρήση υπολογιστικών συστημάτων για την υποστήριξη της ιατρικής απόφασης είναι δυνατόν να αποδειχθεί πολύ χρήσιμη στην πράξη. Συστήματα πληροφορικής μπορούν να προσφέρουν σημαντική βοήθεια σε διάφορες φάσεις της διαγνωστικής διαδικασίας, ιδιαίτερα σε αυτές όπου η γνώση είναι δυνατόν να δομηθεί και χαρακτηρίζεται από τον αντικειμενικό της χαρακτήρα.

Το προτεινόμενο σύστημα με την εφαρμογή τεχνολογιών Τεχνητής Νοημοσύνης και Βάσεων Δεδομένων θα αναπτυχθεί στα προαναφερθέντα πλαίσια και αναμένεται να αποτελέσει σημαντικό βοήθημα στην διάγνωση της παιδικής επιληψίας ιδιαίτερα για τους νέους και τους ειδικευόμενους παιδονευρολόγους. Παράλληλα θα θέσει τις βάσεις για την δημιουργία αντίστοιχης ερευνητικής υποδομής στο ΤΕΙ Κρήτης, η οποία στο μέλλον θα βελτιώσει το υπό ανάπτυξη σύστημα με χρήση και άλλων τεχνολογιών της Πληροφορικής και της Τηλεπληροφορικής και πιθανότατα θα αναπτύξει αντίστοιχα νέα συστήματα σε άλλους τομείς της Ιατρικής, όπου υπάρχει ανάγκη τέτοιων εργαλείων και εκτεταμένο πεδίο έρευνας.[:]