SISTEMA ANALITICO DE DISEÑO DE SOFTWARE.

Sistema analítico de diseño de software dispuesto para recibir especificaciones (14,

18, 22) informales de diseño de sistema, para permitir el desarrollo de diseños (102, 104) de especificaciones formales para una pluralidad de componentes del sistema y para convertir los diseños (102, 104) de especificaciones formales en especificaciones (66, 68, 70, 72) de diseño verificadas para su uso en la creación automática de código (76) fuente y llevar a cabo pruebas de implementación del código (76) fuente, comprendiendo el sistema:

un módulo (91) editor dispuesto para permitir la edición por un usuario de las especificaciones (102, 104) formales para cada componente;

un generador (90) de especificaciones de caja negra verificadas dispuesto para permitir desarrollar las especificaciones (14, 18, 22) informales de diseño de sistema recibidas para cada componente en:

(i) especificaciones (102) formales de diseño representativas de una función de caja negra completamente especificada; y

(ii) especificaciones (104) formales de interfaz representativas de una especificación de caja negra infraespecificada, en el que se consigue una infraespecificación introduciendo predicados indefinidos para capturar, para un estímulo s dado, una pluralidad de posibles respuestas y comportamiento posterior,

en el que las especificaciones (i) y (ii) se desarrollan usando el módulo (91) editor, y el generador (90) de especificaciones de caja negra está dispuesto además para probar la corrección de las especificaciones (102) formales de diseño y especificaciones (104) formales de interfaz y para generar las especificaciones (66, 68, 70, 72) de diseño verificadas;

comprendiendo el generador (90) de especificaciones de caja negra:

medios para presentar, a través del módulo (91) editor, tablas (160) de enumeración para capturar las especificaciones formales como especificaciones basadas en secuencias, en el que cada fila de una tabla identifica un estímulo, su respuesta y su equivalencia;

un generador (106) de modelos dispuesto para generar automáticamente un modelo (108) matemático en notación CSP del comportamiento del sistema para cada componente a partir de las especificaciones (102) formales de diseño y las especificaciones (104) formales de interfaz expresadas en las tablas (160) de enumeración, donde CSP significa Comunicación de Procesos Secuenciales; y

un comprobador (110) de modelos dispuesto para analizar los modelos (108) matemáticos para determinar si tienen el comportamiento requerido para ese componente, para identificar errores en las especificaciones (102) formales de interfaz y en las especificaciones (104) formales de diseño, para realimentar los errores en las especificaciones (102, 104) de diseño informales y/o formales;

en el que el generador (90) de caja negra verificada está dispuesto para permitir a un usuario ajustar las especificaciones (102) formales de interfaz y las especificaciones (104) formales de diseño a través de las tablas (160) de enumeración, para generar modelos (108) matemáticos corregidos, para analizar los mismos, para identificar errores y para realimentar los errores hasta que se consiga el comportamiento requerido para ese componente; y para derivar las especificaciones (66, 68, 70, 72) de diseño verificadas requeridas a partir de los modelos (108) matemáticos libres de errores

Sistema analítico de diseño de software.

Campo de la invención

La presente invención se refiere a un sistema analítico de diseño de software y, más en particular, aunque no exclusivamente, a un sistema de diseño de software que está dispuesto para mejorar la eficacia y la efectividad del desarrollo de software en un entorno industrial aplicando técnicas matemáticas para especificar, modelar y verificar diseños de software antes de que se implementen.

Antecedentes de la invención

En prácticamente todas las ramas reconocidas de la ingeniería, las implementaciones se basan en diseños verificados; es decir, los requisitos funcionales del producto final se especifican de manera rigurosa, se construyen modelos matemáticos para representar estos y los diseños propuestos, y los modelos de diseño se verifican matemáticamente frente a los modelos de requisitos para garantizar que cumplen su función prevista antes de que empiece la implementación.

El software no se desarrolla por lo general de esta forma. La mayor parte de los sistemas de software se especifican mediante especificaciones informales de requisitos que se escriben en lenguaje natural en términos específicos del negocio y el campo por expertos en el campo que generalmente no son expertos en diseño e implementación de software. Se reconoce ampliamente que tales especificaciones adolecen de un carácter incompleto, ambigüedad e inconsistencias; en otras palabras, una falta de rigor y precisión.

Los diseños los realizan expertos en diseño e implementación de software, pero cuyos conocimientos de base del campo a menudo son superficiales o incompletos. Como consecuencia, a menudo no reconocerán las deficiencias de las especificaciones a partir de las cuales trabajan hasta muy avanzada la implementación de la fase de pruebas de un proyecto, si es que lo hacen.

El comportamiento de software integrado, accionado por eventos, es a menudo extremadamente complejo recurriéndose a muchos paralelismos y el diseño debe afrontar numerosas cuestiones relacionadas con la concurrencia. Los errores en tales diseños son habituales porque es extremadamente difícil entender y razonar sistemas concurrentes. En caso de no detectarse, tales errores de diseño llevan a errores de implementación que son extremadamente difíciles de detectar y diagnosticar mediante pruebas porque suelen ser intermitentes en su efecto y difíciles de reproducir.

Como resultado, es habitual lanzar este tipo de software con un gran número de defectos sin descubrir y que estos permanezcan sin detectar durante meses o incluso años.

Resulta útil definir varios términos que se usan a lo largo de esta memoria descriptiva para describir los enfoques de la técnica anterior y las realizaciones de la presente invención (también denominada como el sistema ASD) y estos se exponen a continuación:

Software industrial

Software informático desarrollado principalmente por motivos comerciales. Este tipo de software se desarrolla con fines comerciales y/o constituye un producto previsto para la explotación comercial o constituye una parte de algún otro producto desarrollado a su vez con fines comerciales y/o previsto para su explotación comercial.

El software industrial debe cumplir las normas de calidad normalmente exigidas y esperadas de productos comerciales en el mercado. El software industrial habitualmente necesita tener una vida sostenible de muchos años y poder modificarse y mantenerse por muchos (equipos de) expertos en desarrollo de software diferentes durante su vida.

Esto contrasta con el software desarrollado por individuos u organizaciones académicas, de investigación o de otro tipo por motivos no comerciales tales como promover el conocimiento o por otros motivos cuya principal motivación no es la comercial.

Desarrollo de software industrial

Cualquier actividad para el desarrollo de software industrial. El desarrollo de software industrial se lleva a cabo en un contexto empresarial y está sujeto a limitaciones de coste y tiempo de salida al mercado. A menudo conlleva un esfuerzo de muchos años de desarrollo y se compone de miles y hasta millones de líneas de código de programa fuente y las especificaciones y diseños materializan un extenso conocimiento específico del producto y el campo. La escala y complejidad del desarrollo de software industrial hace que esté fuera de las capacidades de personas individuales y requiere equipos de expertos en desarrollo de software que trabajan junto con especialistas en el producto y el campo.

Diseño de software industrial

Actividades de diseño emprendidas durante el desarrollo de software industrial.

Especificación de caja negra

La especificación del comportamiento visible externamente del componente de software en términos de función matemática absoluta que correlaciona cualquier posible secuencia de estímulos de entrada con la respuesta apropiada. La forma exacta de esta función y su especificación se indica en [PP03]. En el sistema ASD, se emplean dos variedades de especificaciones de función de caja negra:

1. Una función de caja negra infraespecificada se usa para especificar interfaces de componentes de una manera que captura el comportamiento no determinístico habitualmente presente en especificaciones de interfaces porque se especifican a un nivel de abstracción en el que se ocultan detalles de implementación. En el sistema ASD, tales especificaciones también se denominan especificaciones formales de interfaces.

2. Una caja negra totalmente especificada se usa para especificar el diseño de un componente. Siempre se pretende que los diseños de componentes sean determinísticos al nivel de abstracción al que se especifica el comportamiento diseñado. En el sistema ASD, tales especificaciones también se denominan especificaciones formales de diseño de componentes.

Una especificación de caja negra especifica el comportamiento en términos de secuencias de estímulos de entrada y respuestas. No se incluye información de flujo de estado o de control.

Especificación de caja de estado

Una especificación de caja de estado es una refundición de una especificación de caja negra en forma de una función matemática absoluta que correlaciona un par (estado, estímulos) con un par (nuevo estado, respuesta). Las secuencias de estímulos de entrada se sustituyen por datos de estado que capturan la misma información. En el sistema ASD, se requieren especificaciones de caja de estado, también denominadas especificaciones de implementación, únicamente para aquellas partes del software para las que el código fuente de programa no puede generarse automáticamente por el generador de código y por tanto deben programarse a mano. Una caja de estado debe especificar exactamente el mismo comportamiento que la caja negra de la que se deriva.

Requisitos funcionales

Un conjunto de afirmaciones que especifican el comportamiento requerido de un componente o sistema de software. Los requisitos funcionales tienen que ver únicamente con el comportamiento; otras propiedades requeridas del sistema o componente se denominan requisitos no funcionales.

Especificación de interfaz funcional

Una especificación de interfaz que describe el comportamiento de un componente en términos de sus respuestas visibles frente a secuencias de estímulos de entrada en una de sus interfaces.

Especificación de requisitos

Una afirmación de requisitos, funcionales y no funcionales que el sistema o componente de software ha de satisfacer.

Especificación de arquitectura

Una descripción de un sistema de software que identifica sus partes componentes, las interfaces entre esos componentes, las funciones que ha de realizar cada componente y todos los demás requisitos técnicos y reglas de diseño que deben cumplir todos los diseños de componente y especificaciones de interfaz.

Diseño y especificación de componente

La especificación detallada de un componente, su organización y estructura y su comportamiento detallado.

Casos de prueba de componentes

Pruebas diseñadas para probar componentes individuales específicos en cuanto a su corrección frente al diseño y especificación de componente. En el sistema ASD, normalmente se generan automáticamente a partir del diseño por el Generador de casos de prueba en forma de programas de prueba de autoejecución.

Código de programa fuente

La...

1. Sistema analítico de diseño de software dispuesto para recibir especificaciones (14, 18, 22) informales de diseño de sistema, para permitir el desarrollo de diseños (102, 104) de especificaciones formales para una pluralidad de componentes del sistema y para convertir los diseños (102, 104) de especificaciones formales en especificaciones (66, 68, 70, 72) de diseño verificadas para su uso en la creación automática de código (76) fuente y llevar a cabo pruebas de implementación del código (76) fuente, comprendiendo el sistema:

un módulo (91) editor dispuesto para permitir la edición por un usuario de las especificaciones (102, 104) formales para cada componente;

un generador (90) de especificaciones de caja negra verificadas dispuesto para permitir desarrollar las especificaciones (14, 18, 22) informales de diseño de sistema recibidas para cada componente en:

(i) especificaciones (102) formales de diseño representativas de una función de caja negra completamente especificada; y

(ii) especificaciones (104) formales de interfaz representativas de una especificación de caja negra infraespecificada, en el que se consigue una infraespecificación introduciendo predicados indefinidos para capturar, para un estímulo s dado, una pluralidad de posibles respuestas y comportamiento posterior,

en el que las especificaciones (i) y (ii) se desarrollan usando el módulo (91) editor, y el generador (90) de especificaciones de caja negra está dispuesto además para probar la corrección de las especificaciones (102) formales de diseño y especificaciones (104) formales de interfaz y para generar las especificaciones (66, 68, 70, 72) de diseño verificadas;

comprendiendo el generador (90) de especificaciones de caja negra:

medios para presentar, a través del módulo (91) editor, tablas (160) de enumeración para capturar las especificaciones formales como especificaciones basadas en secuencias, en el que cada fila de una tabla identifica un estímulo, su respuesta y su equivalencia;

un generador (106) de modelos dispuesto para generar automáticamente un modelo (108) matemático en notación CSP del comportamiento del sistema para cada componente a partir de las especificaciones (102) formales de diseño y las especificaciones (104) formales de interfaz expresadas en las tablas (160) de enumeración, donde CSP significa Comunicación de Procesos Secuenciales; y

un comprobador (110) de modelos dispuesto para analizar los modelos (108) matemáticos para determinar si tienen el comportamiento requerido para ese componente, para identificar errores en las especificaciones (102) formales de interfaz y en las especificaciones (104) formales de diseño, para realimentar los errores en las especificaciones (102, 104) de diseño informales y/o formales;

en el que el generador (90) de caja negra verificada está dispuesto para permitir a un usuario ajustar las especificaciones (102) formales de interfaz y las especificaciones (104) formales de diseño a través de las tablas (160) de enumeración, para generar modelos (108) matemáticos corregidos, para analizar los mismos, para identificar errores y para realimentar los errores hasta que se consiga el comportamiento requerido para ese componente; y para derivar las especificaciones (66, 68, 70, 72) de diseño verificadas requeridas a partir de los modelos (108) matemáticos libres de errores.

2. Sistema según la reivindicación 1, en el que el sistema está dispuesto para manejar especificaciones informales de diseño de sistema que comprenden especificaciones informales de requisitos, especificaciones informales de arquitectura y diseños de componentes y especificaciones informales.

3. Sistema según la reivindicación 2, en el que el generador (90) de especificaciones de caja negra está dispuesto para permitir la creación de especificaciones (104) formales de interfaz del comportamiento funcional requerido de cada componente que es visible mediante sus interfaces.

4. Sistema según la reivindicación 3, en el que el generador (90) de especificaciones de caja negra está dispuesto para permitir la creación de las especificaciones (104) formales de interfaz como especificaciones de caja negra infraespecificadas del comportamiento funcional requerido.

5. Sistema según cualquiera de las reivindicaciones 2 a 4, en el que el generador (90) de especificaciones de caja negra está dispuesto para permitir la creación de especificaciones (102) formales de diseño de componentes del comportamiento funcional requerido de cada componente.

6. Sistema según la reivindicación 5, en el que el generador (90) de especificaciones de caja negra está dispuesto para permitir la creación de las especificaciones (102) formales de diseño de componentes como especificaciones de caja negra totalmente especificadas del comportamiento funcional requerido.

7. Sistema según la reivindicación 5 ó 6, en el que el generador (90) de especificaciones de caja negra está dispuesto para garantizar que las especificaciones (102) formales de diseño de componentes se crean para ser compatibles con el comportamiento de interfaz requerido.

8. Sistema según cualquier reivindicación anterior, en el que el generador de especificaciones de caja negra está dispuesto para generar una especificación de requisitos verificada, una especificación de arquitectura verificada, una especificación de diseño de componentes verificada y una especificación de interfaces de componentes verificada.

9. Sistema según cualquier reivindicación anterior, en el que el módulo (91) editor está dispuesto para presentar una pantalla (138) de interfaz para permitir al usuario especificar una interfaz de componente, incluyendo la pantalla de interfaz el nombre de la interfaz, un identificador único para cada estímulo y respuesta pertenecientes a la interfaz, una lista de estímulos de entrada, y una lista de respuestas.

10. Sistema según cualquier reivindicación anterior, en el que el módulo editor está dispuesto para presentar tablas (160) de enumeración que están divididas cada una en secciones, una sección para una secuencia canónica que resulta de la especificación basada en secuencias.

11. Sistema según cualquier reivindicación anterior, en el que el generador (90) de especificaciones de caja negra comprende un generador (100) de especificaciones basadas en secuencias para facilitar la creación por el usuario de las especificaciones (102, 104) formales de diseño y de interfaz a partir de las especificaciones (14, 18, 22) informales de diseño de sistema recibidas.

12. Sistema según la reivindicación 11, en el que el generador (100) de especificaciones basadas en secuencias está dispuesto para emitir datos de análisis para su consideración por el usuario de las especificaciones de diseño.

13. Sistema según cualquier reivindicación anterior, en el que el comprobador (110) de modelos comprende un comprobador de modelos FDR para comprobar los modelos matemáticos descritos en notación CSP.

14. Sistema según cualquier reivindicación anterior, en el que el módulo (91) editor está dispuesto para almacenar datos como archivos (93) de datos.

15. Sistema según cualquier reivindicación anterior, que comprende además un generador (92) de código automatizado para crear código (76) fuente de programa generado por máquina a partir de las especificaciones (64) verifica-das.

16. Sistema según cualquier reivindicación anterior, que comprende además un generador (96) de casos de prueba de componentes automatizado para crear casos (78) de prueba de componentes generados por máquina a partir de las especificaciones (64) verificadas.

17. Sistema según la reivindicación 16, en el que el generador (96) de casos de prueba automatizado comprende:

un generador de secuencias de prueba dispuesto para generar un conjunto de casos de prueba en forma de secuencias de estímulos de entrada con las respuestas esperadas;

un generador de programas de prueba que toma los casos de prueba y genera programas de prueba correspondientes a cada caso de prueba; y

un oráculo de prueba que toma archivos de datos, generados por los programas de prueba, que registran los resultados de la prueba y está dispuesto para analizar los resultados para determinar si se ha pasado la prueba.

18. Sistema según cualquier reivindicación anterior, que comprende además un generador (94) de especificaciones de implementación verificadas para ayudar a los usuarios a crear especificaciones (74) de implementación verificadas a partir de las especificaciones (64) verificadas para componentes de software que no pueden generarse automáticamente.

19. Sistema según cualquier reivindicación anterior, que comprende además un generador de verificadores de protocolo de interfaz para crear verificadores de protocolo de interfaz generados por máquina a partir de las especificaciones verificadas.

20. Un soporte de datos que tiene almacenado en el mismo un programa para un ordenador para configurar el ordenador para que funcione como un sistema como se expone en la reivindicación 1.

21. Procedimiento para desarrollar y convertir diseños (102, 104) de especificaciones formales de un sistema de software que va a diseñarse, en especificaciones (66, 68, 70, 72) de diseño verificadas para su uso en la creación automática de código (76) fuente y para llevar a cabo pruebas de implementación del código (76) fuente para el sistema de software, comprendiendo el procedimiento:

recibir especificaciones (14, 18, 22) informales de diseño de sistema para una pluralidad de componentes del sistema de software;

permitir, usando un módulo (91) editor, a un usuario editar las especificaciones (102, 104) formales para cada componente;

proporcionar un generador (90) de especificaciones de caja negra verificadas para:

desarrollar para cada componente, a partir de las especificaciones (14, 18, 22) informales de diseño de sistema recibidas:

(i) especificaciones (102) formales de diseño representativas de una función de caja negra completamente especificada; y

(ii) especificaciones (104) formales de interfaz representativas de una especificación de caja negra infraespecificada, en el que la infraespecificación se consigue introduciendo predicados indefinidos para capturar, para un estímulo s dado, una pluralidad de posibles respuestas y comportamiento posterior,

en el que se desarrollan las especificaciones (i) y (ii) usando el módulo (91) editor,

probando la corrección de las especificaciones (102) formales de diseño y de las especificaciones (104) formales de interfaz;

generando las especificaciones (66, 68, 70, 72) de diseño verificadas;

presentando, a través del módulo (91) editor, tablas (160) de enumeración para capturar las especificaciones formales como especificaciones basadas en secuencias, en el que cada fila de una tabla identifica un estímulo, su respuesta y su equivalencia;

producir automáticamente, usando un generador (106) de modelos, un modelo (108) matemático en notación CSP del comportamiento del sistema para cada componente a partir de las especificaciones (102) formales de diseño y las especificaciones (104) formales de interfaz expresadas en las tablas (160) de enumeración, donde CSP significa Comunicación de Procesos Secuenciales;

analizando, usando un comprobador (110) de modelos, los modelos (108) matemáticos para determinar si tienen el comportamiento requerido para ese componente, para identificar errores en las especificaciones (102) formales de interfaz y las especificaciones (104) formales de diseño, y para realimentar los errores en las especificaciones (102, 104) informales y/o formales de diseño; y

usando el generador (90) de especificaciones de caja negra para permitir a un usuario ajustar las especificaciones (102) formales de interfaz y las especificaciones (104) formales de diseño a través de las tablas (160) de enumeración, para generar modelos (108) matemáticos corregidos, para analizar los mismos, para identificar errores y para realimentar los errores hasta que se consiga el comportamiento requerido para ese componente; y para derivar las especificaciones (66, 68, 70, 72) de diseño verificadas requeridas a partir de los modelos (108) matemáticos libres de errores.